| Age | Commit message (Expand) | Author |
|---|
| 2009-09-18 | - Fixed a bug in checking that implicit arguments are all correctly | herbelin |
| 2009-09-17 | Remove useless Liboject.export_function field | glondu |
| 2009-09-17 | Delete trailing whitespaces in all *.{v,ml*} files | glondu |
| 2009-09-10 | Added syntax "exists bindings, ..., bindings" for iterated "exists". | herbelin |
| 2009-08-13 | Death of "survive_module" and "survive_section" (the first one was | herbelin |
| 2009-08-06 | - Cleaning phase of the interfaces of libnames.ml and nametab.ml | herbelin |
| 2009-08-03 | Added "etransitivity". | herbelin |
| 2009-07-15 | - Fixing bug #2139 (kernel-based test of well-formation of elimination | herbelin |
| 2009-07-08 | Reactivation of pattern unification of evars in apply unification, in | herbelin |
| 2009-07-07 | Jolification : tentative de supprimer les "( evd)" et associés qui | aspiwack |
| 2009-06-11 | Use a lazy value for the message in FailError, so that it won't be | msozeau |
| 2009-06-06 | Fixing bug 2110 (tactic "refine" was calling (co)mutual_fix with index 0 | herbelin |
| 2009-06-02 | Backtrack on experimental unification with sort variables: it requires | msozeau |
| 2009-05-23 | A try at using sort variables during unification. Instead of refreshing | msozeau |
| 2009-05-20 | - Fixing declarative mode in presence of high use of Change_evars nodes | herbelin |
| 2009-05-18 | Minor unification changes: | msozeau |
| 2009-04-24 | Fixing bug #2308 ("instantiate" tactic did not comply with | herbelin |
| 2009-03-20 | Many changes in the Makefile infrastructure + a beginning of ocamlbuild | letouzey |
| 2009-03-16 | Cleaning/improving the use of the "in" clause (e.g. "unfold foo in H at 4" | herbelin |
| 2009-03-14 | Cleaning/uniformizing the interface of tacticals.mli | herbelin |
| 2009-03-04 | commande Timeout + compaction des traces de debug_tactic | barras |
| 2009-02-19 | On remplace evar_map par evar_defs (seul evar_defs est désormais exporté | aspiwack |
| 2009-02-06 | pushed evar reduction in kernel | barras |
| 2009-01-23 | Really compare evar maps in progress, due to merging in apply and other | msozeau |
| 2009-01-18 | Backporting from v8.2 to trunk: | herbelin |
| 2009-01-04 | Fixed bugs #2001 (search_guard was overwriting the guard index given | herbelin |
| 2008-12-29 | - Added support for subterm matching in SearchAbout. | herbelin |
| 2008-12-26 | - Optimized "auto decomp" which had a (presumably) exponential in | herbelin |
| 2008-12-14 | Fix looping class resolution bug discovered by B. Aydemir and use the | msozeau |
| 2008-12-09 | About "apply in": | herbelin |
| 2008-11-27 | fixing problem with CompCert: reordering resulting from tac change was not cl... | barras |
| 2008-11-26 | closed bug 1898: fold x in x; added a reordering primitive tactic | barras |
| 2008-10-26 | Fixes and refinements regarding occurrence selection: | herbelin |
| 2008-10-26 | Backtrack sur commit 11467 (tentative d'optimisation meta_instance qui | herbelin |
| 2008-10-25 | More debugging of handling of open constrs with typeclasses: | msozeau |
| 2008-10-25 | Fix for bug #1981, correct the mismatch between the meta types used in | msozeau |
| 2008-10-24 | Raise informative errors instead of Failures or anomalies in case a meta | msozeau |
| 2008-10-19 | - Export de pattern_ident vers les ARGUMENT EXTEND and co. | herbelin |
| 2008-10-18 | Optimisation de clenv.ml pour que meta_instance ne soit pas appelé | herbelin |
| 2008-10-07 | fixing r11433 again: | barras |
| 2008-10-06 | bug #1951: polymorphic indtypes: universe subst was not performed in the type... | barras |
| 2008-09-09 | Correction bug assert (introduit dans la révision 11300) qui ne | herbelin |
| 2008-09-07 | More debugging of [Equations], now able to discharge even the heavily | msozeau |
| 2008-08-05 | Correction de bugs: | herbelin |
| 2008-08-04 | Évolutions diverses et variées. | herbelin |
| 2008-07-18 | - Rebranchement backtrack du langage déclaratif dans Coqide | herbelin |
| 2008-07-18 | Modification rapide du message d'erreur lorsqu'un _ ne peut être | herbelin |
| 2008-06-27 | Changement de catch_error pour qu'il rattrape les erreurs d'arguments | aspiwack |
| 2008-06-21 | - Implantation de la suggestion 1873 sur discriminate. Au final, | herbelin |
| 2008-06-16 | Add possibility to match on defined hypotheses, using brackets to | msozeau |
