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