The Coq mailing list

[Pierre Boutillier <pierre.boutillier AT inria.fr>]

Hi list,

I am currently going though the "trunk" bugs of Coq in order to tag the one that need to be fix before v8.4 release commenting dozens of:
"This bug should be fixed before v8.4 release."

I'm sorry  but coqdevs won't be able to handle them in a reasonable amount of time. My hope in order not to fall in depression is that for some of them advanced users among you could maybe help us. For example, on the following example: http://www.lix.polytechnique.fr/coq/bugs/show_bug.cgi?id=2630

The easy tactic is written in ltac. In its code http://coq.inria.fr/distrib/V8.4beta/stdlib/Coq.Init.Tactics.html, you can see a "reflexivity". Anyway, it does not work in the

Require Import QArith.

Lemma kaas (x:Q) : Qle x x.
  unfold Qle.
  (* fails: easy. *)
  (* works: *) reflexivity.
Qed.

example. Can an Ltac expert can see why ?

Thanks in advance if you accept to spare time on that and help is really, really, really, enjoyed in any example of http://www.lix.polytechnique.fr/coq/bugs/report.cgi?x_axis_field=version&y_axis_field=component&z_axis_field=&query_format=report-table&short_desc_type=allwordssubstr&short_desc=&long_desc_type=allwordssubstr&long_desc=&bug_file_loc_type=allwordssubstr&bug_file_loc=&deadlinefrom=&deadlineto=&bug_status=UNCONFIRMED&bug_status=NEW&bug_status=ASSIGNED&bug_status=REOPENED&emailassigned_to1=1&emailtype1=substring&email1=&emailassigned_to2=1&emailreporter2=1&emailcc2=1&emailtype2=substring&email2=&bugidtype=include&bug_id=&chfieldfrom=&chfieldto=Now&chfieldvalue=&format=table&action="wrap&field0-0-0=noop&type0-0-0=noop&value0-0-0=
(btw it is the exact moment to make fun of us and say that the solution is "info" :-) but please troll kindly)

All the best
Pierre Boutillier