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