| Age | Commit message (Expand) | Author |
|---|
| 2010-04-29 | Remove the svn-specific $Id$ annotations | letouzey |
| 2010-04-22 | Here comes the commit, announced long ago, of the new tactic engine. | aspiwack |
| 2009-12-21 | Generic support for open terms in tactics | herbelin |
| 2009-09-18 | - Fixed a bug in checking that implicit arguments are all correctly | herbelin |
| 2009-09-17 | Delete trailing whitespaces in all *.{v,ml*} files | glondu |
| 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-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-18 | Minor unification changes: | msozeau |
| 2009-04-24 | Fixing bug #2308 ("instantiate" tactic did not comply with | herbelin |
| 2009-02-19 | On remplace evar_map par evar_defs (seul evar_defs est désormais exporté | aspiwack |
| 2008-12-14 | Fix looping class resolution bug discovered by B. Aydemir and use the | msozeau |
| 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-24 | Raise informative errors instead of Failures or anomalies in case a meta | msozeau |
| 2008-10-18 | Optimisation de clenv.ml pour que meta_instance ne soit pas appelé | herbelin |
| 2008-06-21 | - Implantation de la suggestion 1873 sur discriminate. Au final, | herbelin |
| 2008-04-27 | - Backtrack sur option with_types suite à confusion sur l'utilisation | herbelin |
| 2008-04-26 | - Backtrack sur extension de syntaxe pour pose qui rentre en conflit avec | herbelin |
| 2008-04-21 | - Parameterize unification by two sets of transparent_state, one for open | msozeau |
| 2008-04-17 | Bug squashing day ! | msozeau |
| 2008-04-13 | Bugs, nettoyage, et améliorations diverses | herbelin |
| 2008-03-16 | Using the "relation" constant made some unifications fail in the new | msozeau |
| 2008-02-13 | Essai de prise en compte de delta dans unify_0 (même sur termes non clos). | herbelin |
| 2007-10-03 | Ajout de eelim, ecase, edestruct et einduction (expérimental). | herbelin |
| 2007-05-29 | Correction d'un bug dans l'affichage du message d'erreur real_clean | herbelin |
| 2007-05-20 | - Propagation des evars non résolues vers les with_bindings; permet par exemple | herbelin |
| 2006-02-10 | induction now admits multiple induction arguments. The principle must | coq |
| 2005-12-02 | Changement des named_context | gregoire |
| 2004-10-20 | COMMITED BYTECODE COMPILER | barras |
| 2004-09-17 | restructuration des printers: proofs passe avant parsing | barras |
| 2004-09-12 | inclusion de meta_map dans evar_defs | barras |
| 2004-09-10 | simplification de clenv | barras |
| 2004-09-08 | unification encore... | barras |
| 2004-09-07 | deuxieme vague de modifs: evar_defs fonctionnel | barras |
| 2004-09-03 | premiere reorganisation de l\'unification | barras |
