The Coq mailing list

[Pierre Boutillier <pierre.boutillier AT pps.univ-paris-diderot.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 "info" could  
help :-) but please troll kindly)

All the best
Pierre Boutillier