| Age | Commit message (Expand) | Author |
|---|
| 2012-06-04 | Forward-port fixes from 8.4 (15358, 15353, 15333). | msozeau |
| 2012-03-20 | Fix interface of resolve_typeclasses: onlyargs -> with_goals: | msozeau |
| 2012-03-02 | Noise for nothing | pboutill |
| 2011-12-17 | Added a flag to control the use of typing when instantiating applied | herbelin |
| 2011-10-11 | Moved to a more standard order of arguments (i.e. env followed by evar_map) | herbelin |
| 2011-06-18 | Generalizing flag use_evars_pattern_unification into a flag | herbelin |
| 2011-06-13 | Added a flag to restrict conversion in tactic unification on the | herbelin |
| 2011-06-12 | Added a new flag for freezing evars in tactic unification. Used this | herbelin |
| 2011-06-10 | Moved allow_K to a unification flag | herbelin |
| 2011-04-18 | Add a flag to control betaiota reduction during unification to maintain backw... | msozeau |
| 2011-03-13 | - Add modulo_delta_types flag for unification to allow full | msozeau |
| 2010-12-23 | Rename rawterm.ml into glob_term.ml | glondu |
| 2010-09-20 | Added eta-expansion in kernel, type inference and tactic unification, | herbelin |
| 2010-09-17 | In the computation of missing arguments for apply, accept that the | herbelin |
| 2010-07-24 | Updated all headers for 8.3 and trunk | herbelin |
| 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 |
