Andrej Dudenhefner comments

Results 55 comments of


                                            Andrej Dudenhefner

Consider changing to a permissive or weak copyleft license

> In that case, I would only migrate the current living branch, namely the `coq-8.17` branch. For migration, I'd suggest the `master` branch, which will be `coq-8.18` (I guess we...

[stdlib] Add `Proper` instances for some number theorems to improve rewriting with inequalities

The combination of all - `Proper (eq ==> lt ==> lt) add` - `Proper (lt ==> eq ==> lt) add` - `Proper (lt ==> lt ==> lt) add` - `Proper...

[stdlib] Add `Proper` instances for some number theorems to improve rewriting with inequalities

> @mrhaandi I will gladly remove those instances, but could you explain why this would lead to poor performance? Having every possible combination of `le`, `lt`, `eq` as hint introduces...

"fix" tactic may produce ill formed terms

Here is a related discrepancy with `fix`, which could possibly help to debug the issue: ```coq Goal unit -> unit. Proof. refine (fix F (H : unit) : unit :=...

"fix" tactic may produce ill formed terms

I'm not sure whether eta is the exact issue here. The following code does not fail. ```coq Goal unit -> unit. Proof. fix F 1. Show Proof. (* (fix F...