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