aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/evarutil.mli
Commit message (Expand)AuthorAge
* 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
* Continuing r1492 (useless changes were inadvertantly committed)Gravatar herbelin2011-10-25
* New strategy to infer return predicate of match construct whenGravatar herbelin2011-10-25
* More robust and uniform treatment of aliases in evarutil.mlGravatar herbelin2011-10-10
* Applied the trick of Chung-Kil Hur to solve second-order matchingGravatar herbelin2011-10-10
* Passed conv_algo to evar_define and move call to solve_refl toGravatar herbelin2011-10-10
* - Fix restrict_hyps to not allow filtering on a variable required to typechec...Gravatar msozeau2011-06-07
* Tentative to make unification check types at every instanciation of anGravatar msozeau2011-03-11
* - Better error messages taking unif. constraints into account.Gravatar msozeau2011-03-11
* Reverted commit r13893 about propagation of more informativeGravatar herbelin2011-03-07
* Added propagation of evars unification failure reasons for betterGravatar herbelin2011-03-07
* Improved define_evar_as_lambda which was creating an unrelated new evarGravatar herbelin2011-03-05
* Repair Class_tactics.split_evars, broken by r13717 (should fix #2481)Gravatar letouzey2011-02-03
* mli comments for docGravatar pboutill2011-01-07
* Rename rawterm.ml into glob_term.mlGravatar glondu2010-12-23
* Misc improvements about evar_mapGravatar letouzey2010-12-15
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* Made tclABSTRACT normalize evars before saying it does not supportGravatar herbelin2010-06-29
* New script dev/tools/change-header to automatically update Coq files headers.Gravatar herbelin2010-06-22
* Fixing Derive Inversion for new proof engineGravatar herbelin2010-05-26
* Improved the efficiency of evars traverals thanks to a split ofGravatar herbelin2010-05-13
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* Move from ocamlweb to ocamdoc to generate mli documentationGravatar pboutill2010-04-29