index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
pretyping
/
evarutil.mli
Commit message (
Expand
)
Author
Age
*
Reuse universe level substitutions for template polymorphism, fixing performance
Matthieu Sozeau
2014-05-09
*
- Fix treatment of global universe constraints which should be passed along
Matthieu Sozeau
2014-05-06
*
Try a new way of handling template universe levels
Matthieu Sozeau
2014-05-06
*
This commit adds full universe polymorphism and fast projections to Coq.
Matthieu Sozeau
2014-05-06
*
Remove many superfluous 'open' indicated by ocamlc -w +33
Pierre Letouzey
2014-03-05
*
Removing useless meta-related functions.
Pierre-Marie Pédrot
2013-12-03
*
A newly introduced variable inside a named context is no longer α-renamed.
aspiwack
2013-11-02
*
Abstracting evar filter away. The API is not perfect, but better than nothing.
ppedrot
2013-10-27
*
Removing useless evar-related stuff.
ppedrot
2013-09-25
*
At least made the evar type opaque! There are still 5 remaining unsafe
ppedrot
2013-09-18
*
Removing almost all new_untyped_evar, and a bunch of Evd.add.
ppedrot
2013-09-18
*
Partly replacing list-based access functions in Evd. This is still
ppedrot
2013-09-03
*
Replacing lists by sets in clear tactic.
ppedrot
2013-08-25
*
Mini documentation (evar_absorb_arguments).
herbelin
2013-05-14
*
Merging Context and Sign.
ppedrot
2013-04-29
*
Splitting Term into five unrelated interfaces:
ppedrot
2013-04-29
*
Continuation of r16346 on filtering local definitions. Refined
herbelin
2013-03-30
*
Allowing different types of, not to be mixed, generic Stores through
ppedrot
2013-03-12
*
Splitted Evarutil in two files
ppedrot
2013-02-10
*
Moved code from Pretype_error to Evarutil
ppedrot
2013-02-10
*
Modulification of name
ppedrot
2012-12-18
*
Modulification of identifier
ppedrot
2012-12-14
*
Moved Intset and Intmap to Int namespace.
ppedrot
2012-12-14
*
Updating headers.
herbelin
2012-08-08
*
Another correction to the dependent existential variable printing
aspiwack
2012-07-10
*
Added an indirection with respect to Loc in Compat. As many [open Compat]
ppedrot
2012-06-22
*
remove many excessive open Util & Errors in mli's
letouzey
2012-05-29
*
Evar_kinds.mli containing former Evd.hole_kind, avoid deps on Evd
letouzey
2012-05-29
*
Unification: Added a heuristic to solve problems of the form
herbelin
2012-03-26
*
Generalized the use of evar candidates in type inference unification:
herbelin
2012-03-20
*
Remove support for "abstract typing constraints" that requires unicity of sol...
msozeau
2012-03-14
*
Noise for nothing
pboutill
2012-03-02
*
Introducing a notion of evar candidates to be used when an evar is
herbelin
2011-12-16
*
Discarding let-ins from the instances of the evars in the
herbelin
2011-12-04
*
Adds a pair of function in Evar_util to gather dependent evars in an
aspiwack
2011-11-23
*
Fixing incorrect change to pattern-unification over Meta's introduced
herbelin
2011-11-06
*
Continuing r1492 (useless changes were inadvertantly committed)
herbelin
2011-10-25
*
New strategy to infer return predicate of match construct when
herbelin
2011-10-25
*
More robust and uniform treatment of aliases in evarutil.ml
herbelin
2011-10-10
*
Applied the trick of Chung-Kil Hur to solve second-order matching
herbelin
2011-10-10
*
Passed conv_algo to evar_define and move call to solve_refl to
herbelin
2011-10-10
*
- Fix restrict_hyps to not allow filtering on a variable required to typechec...
msozeau
2011-06-07
*
Tentative to make unification check types at every instanciation of an
msozeau
2011-03-11
*
- Better error messages taking unif. constraints into account.
msozeau
2011-03-11
*
Reverted commit r13893 about propagation of more informative
herbelin
2011-03-07
*
Added propagation of evars unification failure reasons for better
herbelin
2011-03-07
*
Improved define_evar_as_lambda which was creating an unrelated new evar
herbelin
2011-03-05
*
Repair Class_tactics.split_evars, broken by r13717 (should fix #2481)
letouzey
2011-02-03
*
mli comments for doc
pboutill
2011-01-07
*
Rename rawterm.ml into glob_term.ml
glondu
2010-12-23
[next]