aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/unification.mli
Commit message (Expand)AuthorAge
* [api] Move structures deprecated in the API to the core.Gravatar Emilio Jesus Gallego Arias2017-11-06
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
* Remove the Sigma (monotonous state) API.Gravatar Maxime Dénès2017-06-06
* unification.mli: Fix a spelling typo in a commentGravatar Jason Gross2017-05-23
* Merge branch 'master' into econstrGravatar Pierre-Marie Pédrot2017-04-07
|\
| * Ensuring static invariants about handling of pending evars in Pretyping.Gravatar Pierre-Marie Pédrot2017-03-23
* | Definining EConstr-based contexts.Gravatar Pierre-Marie Pédrot2017-02-14
* | Unification API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
|/
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
|\
| * Update copyright headers.Gravatar Maxime Dénès2016-01-20
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-13
|\|
| * Fix essential bug in new Keyed Unification mode reported by R. Krebbers.Gravatar Matthieu Sozeau2016-01-12
* | CLEANUP: kernel/context.ml{,i}Gravatar Matej Kosik2016-01-11
* | More monotonicity in Tactics.Gravatar Pierre-Marie Pédrot2015-10-19
|/
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-28 23:23:36 +0000