aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/unification.mli
Commit message (Expand)AuthorAge
* Update headers.Gravatar Maxime Dénès2015-01-12
* Follow up to experimental eager evar unification in bcba6d1bc9:Gravatar Hugo Herbelin2014-11-08
* Enlarge the cases where the like first selection is used in destruct.Gravatar Hugo Herbelin2014-10-31
* Fixing destruct/induction with a using clause on a non-inductive type,Gravatar Hugo Herbelin2014-10-26
* This commit introduces changes in induction and destruct.Gravatar Hugo Herbelin2014-10-25
* A step towards better differentiating when w_unify is used for subtermGravatar Hugo Herbelin2014-09-10
* Made the subterm finding function make_abstraction independent of theGravatar Hugo Herbelin2014-06-28
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-06
* Removing dead code, thanks to new OCaml warnings and a bit of scripting.Gravatar Pierre-Marie Pédrot2014-04-23
* At least made the evar type opaque! There are still 5 remaining unsafeGravatar ppedrot2013-09-18
* export Unification.abstract_list_all_with_dependenciesGravatar pboutill2013-05-30
* Fixed a little inefficiency of "set/destruct" over a pattern. NowGravatar herbelin2012-12-18
* Improving error message when abtraction over goal (abstract_list_allGravatar herbelin2012-10-04
* Updating headers.Gravatar herbelin2012-08-08
* Added a flag to control the use of typing when instantiating appliedGravatar herbelin2011-12-17
* Moved to a more standard order of arguments (i.e. env followed by evar_map)Gravatar herbelin2011-10-11
* Fix unification: detect invalid evar instantiations due to scoping earlier.Gravatar msozeau2011-08-04
* Generalizing flag use_evars_pattern_unification into a flagGravatar herbelin2011-06-18
* Added a flag to restrict conversion in tactic unification on theGravatar herbelin2011-06-13
* Added a new flag for freezing evars in tactic unification. Used thisGravatar herbelin2011-06-12
* Moved allow_K to a unification flagGravatar herbelin2011-06-10
* Add a flag to control betaiota reduction during unification to maintain backw...Gravatar msozeau2011-04-18
* - Add modulo_delta_types flag for unification to allow fullGravatar msozeau2011-03-13
* Added eta-expansion in kernel, type inference and tactic unification,Gravatar herbelin2010-09-20
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* New script dev/tools/change-header to automatically update Coq files headers.Gravatar herbelin2010-06-22
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* Move from ocamlweb to ocamdoc to generate mli documentationGravatar pboutill2010-04-29
* Promote evar_defs to evar_map (in Evd)Gravatar glondu2009-11-11
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* Reactivation of pattern unification of evars in apply unification, inGravatar herbelin2009-07-08
* Add new variants of [rewrite] and [autorewrite] which differ in theGravatar msozeau2009-06-30
* Minor unification changes:Gravatar msozeau2009-05-18
* - Backtrack sur option with_types suite à confusion sur l'utilisationGravatar herbelin2008-04-27
* - Backtrack sur extension de syntaxe pour pose qui rentre en conflit avecGravatar herbelin2008-04-26
* Prise en compte des coercions dans les clauses "with" même si le typeGravatar herbelin2008-04-23
* - Parameterize unification by two sets of transparent_state, one for openGravatar msozeau2008-04-21
* Bug squashing day !Gravatar msozeau2008-04-17
* Ajout "simple apply" et "simple eapply" pour apply sans unfoldGravatar herbelin2008-04-01
* Using the "relation" constant made some unifications fail in the newGravatar msozeau2008-03-16
* Essai de prise en compte de delta dans unify_0 (même sur termes non clos). Gravatar herbelin2008-02-13
* Mise en place d'une toute petite amélioration de l'unification deGravatar herbelin2008-02-07
* Ajout de eelim, ecase, edestruct et einduction (expérimental).Gravatar herbelin2007-10-03
* Contrôle de la compatibilité de apply via une information dans lesGravatar herbelin2007-05-28
* ?(mod_delta=true) parameter added to each unification function.Gravatar sacerdot2004-09-27
* restructuration des printers: proofs passe avant parsingGravatar barras2004-09-17
* hiding the meta_map in evar_defsGravatar barras2004-09-15
* inclusion de meta_map dans evar_defsGravatar barras2004-09-12
* unification encore...Gravatar barras2004-09-08
* deuxieme vague de modifs: evar_defs fonctionnelGravatar barras2004-09-07