coqbot

Comment author: @gares It seems to me this is for "trunk" + "major redesign".

Comment author: @robbertkrebbers Apparently the injection tactic unfolds definitions too eagerly. For example: ``` Fixpoint big (n : nat) := match n with | 0 => 2 | S n...

Comment author: @robbertkrebbers To make things even worse, it even reduces under lambdas! ``` Fixpoint big (n : nat) := match n with | 0 => 2 | S n...

Comment author: @robbertkrebbers At last Coq meeting, Hugo Herbelin looked at this bug for me, and tracked the problem down to line 1077 in tactics/equality.ml4 where simpl is used to...

Comment author: @robbertkrebbers Just another strange observation: even when making foo, bar, and wf_guard Opaque, injection still loops. Also, when declaring these constants as "simpl never" using the Arguments command,...

Comment author: @pirbo Even without `simpl` at the end : In order not to add equality between convertible terms, line 570 of `tactics/equality.ml` tests the convertibility of `n` and `big...

Comment author: @JasonGross I expect this code to work, not to fail at [Check]/[Definition] ``` Class A := a : True. Check _ : A. (* succeeds, leaves an evar...

Comment author: @silene I don't expect this code to work. "abstract" inside a typeclass hint should most certainly fail, since it causes commands that are not allowed to have side-effects...

Comment author: @JasonGross I think the [Definition] command, at least, should succeed; if Definition foo : bar. Proof. refine x. Defined. works, then Definition foo : bar := x. should...

Comment author: @JasonGross It's cool that [match _, _ with] with use typing information from the first one in matching on the second one. It's neat (albeit perhaps a bit...