| Age | Commit message (Expand) | Author |
|---|
| 2016-01-21 | Merge branch 'v8.5' | Pierre-Marie Pédrot |
| 2016-01-20 | Update copyright headers. | Maxime Dénès |
| 2016-01-13 | Merge branch 'v8.5' | Pierre-Marie Pédrot |
| 2016-01-12 | Fix essential bug in new Keyed Unification mode reported by R. Krebbers. | Matthieu Sozeau |
| 2016-01-11 | CLEANUP: kernel/context.ml{,i} | Matej Kosik |
| 2015-10-19 | More monotonicity in Tactics. | Pierre-Marie Pédrot |
| 2015-01-12 | Update headers. | Maxime Dénès |
| 2014-11-08 | Follow up to experimental eager evar unification in bcba6d1bc9: | Hugo Herbelin |
| 2014-10-31 | Enlarge the cases where the like first selection is used in destruct. | Hugo Herbelin |
| 2014-10-26 | Fixing destruct/induction with a using clause on a non-inductive type, | Hugo Herbelin |
| 2014-10-25 | This commit introduces changes in induction and destruct. | Hugo Herbelin |
| 2014-09-10 | A step towards better differentiating when w_unify is used for subterm | Hugo Herbelin |
| 2014-06-28 | Made the subterm finding function make_abstraction independent of the | Hugo Herbelin |
| 2014-05-06 | This commit adds full universe polymorphism and fast projections to Coq. | Matthieu Sozeau |
| 2014-04-23 | Removing dead code, thanks to new OCaml warnings and a bit of scripting. | Pierre-Marie Pédrot |
| 2013-09-18 | At least made the evar type opaque! There are still 5 remaining unsafe | ppedrot |
| 2013-05-30 | export Unification.abstract_list_all_with_dependencies | pboutill |
| 2012-12-18 | Fixed a little inefficiency of "set/destruct" over a pattern. Now | herbelin |
| 2012-10-04 | Improving error message when abtraction over goal (abstract_list_all | herbelin |
| 2012-08-08 | Updating headers. | herbelin |
| 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-08-04 | Fix unification: detect invalid evar instantiations due to scoping earlier. | msozeau |
| 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-09-20 | Added eta-expansion in kernel, type inference and tactic unification, | herbelin |
| 2010-07-24 | Updated all headers for 8.3 and trunk | herbelin |
| 2010-06-22 | New script dev/tools/change-header to automatically update Coq files headers. | herbelin |
| 2010-04-29 | Remove the svn-specific $Id$ annotations | letouzey |
| 2010-04-29 | Move from ocamlweb to ocamdoc to generate mli documentation | pboutill |
| 2009-11-11 | Promote evar_defs to evar_map (in Evd) | glondu |
| 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-06-30 | Add new variants of [rewrite] and [autorewrite] which differ in the | msozeau |
| 2009-05-18 | Minor unification changes: | msozeau |
| 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-23 | Prise en compte des coercions dans les clauses "with" même si le type | 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-01 | Ajout "simple apply" et "simple eapply" pour apply sans unfold | 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 |
| 2008-02-07 | Mise en place d'une toute petite amélioration de l'unification de | herbelin |
| 2007-10-03 | Ajout de eelim, ecase, edestruct et einduction (expérimental). | herbelin |
| 2007-05-28 | Contrôle de la compatibilité de apply via une information dans les | herbelin |
