aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/evarutil.mli
Commit message (Expand)AuthorAge
* Update headers.Gravatar Maxime Dénès2015-01-12
* Tentatively more informative report of failure when inferringGravatar Hugo Herbelin2014-12-11
* Occur-check in refine.Gravatar Arnaud Spiwack2014-12-04
* Move the handling of the principal evar from refine to evd.Gravatar Arnaud Spiwack2014-10-16
* A few Global.env removed.Gravatar Hugo Herbelin2014-10-04
* Add syntax for naming new goals in refine: writing ?[id] instead of _Gravatar Hugo Herbelin2014-09-30
* Merging some functions from evarutil.ml/evd.ml.Gravatar Hugo Herbelin2014-09-29
* Providing a -type-in-type option for collapsing the universe hierarchy.Gravatar Hugo Herbelin2014-09-13
* Uniformisation of the order of arguments env and sigma.Gravatar Hugo Herbelin2014-09-12
* Referring to evars by names. Added a parser for evars (but parsing ofGravatar Hugo Herbelin2014-09-12
* - Fix has_undefined_evars not using its or_sorts argument anymore.Gravatar Matthieu Sozeau2014-08-03
* Add interface function to replace new_Type ()Gravatar Matthieu Sozeau2014-07-14
* Cleanup treatment of template universe polymorphism (thanks to E. TassiGravatar Matthieu Sozeau2014-06-20
* Fixing "clear" in internal_cut_replace: forbid dependencies in theGravatar Hugo Herbelin2014-06-13
* Reuse universe level substitutions for template polymorphism, fixing performanceGravatar Matthieu Sozeau2014-05-09
* - Fix treatment of global universe constraints which should be passed alongGravatar Matthieu Sozeau2014-05-06
* Try a new way of handling template universe levelsGravatar Matthieu Sozeau2014-05-06
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-06
* Remove many superfluous 'open' indicated by ocamlc -w +33Gravatar Pierre Letouzey2014-03-05
* Removing useless meta-related functions.Gravatar Pierre-Marie Pédrot2013-12-03
* A newly introduced variable inside a named context is no longer α-renamed.Gravatar aspiwack2013-11-02
* Abstracting evar filter away. The API is not perfect, but better than nothing.Gravatar ppedrot2013-10-27
* Removing useless evar-related stuff.Gravatar ppedrot2013-09-25
* At least made the evar type opaque! There are still 5 remaining unsafeGravatar ppedrot2013-09-18
* Removing almost all new_untyped_evar, and a bunch of Evd.add.Gravatar ppedrot2013-09-18
* Partly replacing list-based access functions in Evd. This is stillGravatar ppedrot2013-09-03
* Replacing lists by sets in clear tactic.Gravatar ppedrot2013-08-25
* Mini documentation (evar_absorb_arguments).Gravatar herbelin2013-05-14
* Merging Context and Sign.Gravatar ppedrot2013-04-29
* Splitting Term into five unrelated interfaces:Gravatar ppedrot2013-04-29
* Continuation of r16346 on filtering local definitions. RefinedGravatar herbelin2013-03-30
* Allowing different types of, not to be mixed, generic Stores throughGravatar ppedrot2013-03-12
* Splitted Evarutil in two filesGravatar ppedrot2013-02-10
* Moved code from Pretype_error to EvarutilGravatar ppedrot2013-02-10
* Modulification of nameGravatar ppedrot2012-12-18
* Modulification of identifierGravatar ppedrot2012-12-14
* Moved Intset and Intmap to Int namespace.Gravatar ppedrot2012-12-14
* Updating headers.Gravatar herbelin2012-08-08
* Another correction to the dependent existential variable printingGravatar aspiwack2012-07-10
* Added an indirection with respect to Loc in Compat. As many [open Compat]Gravatar ppedrot2012-06-22
* remove many excessive open Util & Errors in mli'sGravatar letouzey2012-05-29
* Evar_kinds.mli containing former Evd.hole_kind, avoid deps on EvdGravatar letouzey2012-05-29
* Unification: Added a heuristic to solve problems of the formGravatar herbelin2012-03-26
* Generalized the use of evar candidates in type inference unification:Gravatar herbelin2012-03-20
* Remove support for "abstract typing constraints" that requires unicity of sol...Gravatar msozeau2012-03-14
* Noise for nothingGravatar pboutill2012-03-02
* Introducing a notion of evar candidates to be used when an evar isGravatar herbelin2011-12-16
* Discarding let-ins from the instances of the evars in theGravatar herbelin2011-12-04
* Adds a pair of function in Evar_util to gather dependent evars in anGravatar aspiwack2011-11-23
* Fixing incorrect change to pattern-unification over Meta's introducedGravatar herbelin2011-11-06