aboutsummaryrefslogtreecommitdiff
path: root/pretyping/evarutil.ml
AgeCommit message (Expand)Author
2012-09-14The new ocaml compiler (4.00) has a lot of very cool warnings,regisgia
2012-08-08Updating headers.herbelin
2012-07-29Fixing #2836 (materialize_evar might refine as a side effect theherbelin
2012-07-10Another correction to the dependent existential variable printingaspiwack
2012-07-06Fixes bug #2678aspiwack
2012-06-22Added an indirection with respect to Loc in Compat. As many [open Compat]ppedrot
2012-06-01More cleaningppedrot
2012-05-29Evar_kinds.mli containing former Evd.hole_kind, avoid deps on Evdletouzey
2012-04-18Corrects a bug in the refine tactic which could drop evar bodies.aspiwack
2012-04-16Fixing a "Not_Found" bug related to commit 15061 on the use of evar candidates.herbelin
2012-04-05Speedup free_vars_and_rels_up_alias_expansion (evarconv)gareuselesinge
2012-03-26Unification: Fixing bug in materialize_evar (spotted by MathClasses).herbelin
2012-03-26Unification: Added a heuristic to solve problems of the formherbelin
2012-03-23Little bug in r15061 leading to unusable debug mode.herbelin
2012-03-20Use a careful analysis of dependencies in restricting instances toherbelin
2012-03-20Unification: when matching "?n[...,(C u1..un),...] = C u1..un" keep aherbelin
2012-03-20Generalized the use of evar candidates in type inference unification:herbelin
2012-03-20Reorganizing the structure of evarutil.ml (only restructuration, noherbelin
2012-03-14Remove support for "abstract typing constraints" that requires unicity of sol...msozeau
2012-03-02Noise for nothingpboutill
2012-02-15Fix in evarutil: add a conversion problem for ?x ts = ?x us only if ts and us...msozeau
2012-01-04Type inference unification: fixed a 8.4 bug in the presence of unificationherbelin
2011-12-16Introducing a notion of evar candidates to be used when an evar isherbelin
2011-12-05Registering universe and meta/evar counters as summaries so as toherbelin
2011-12-05Yet another fix about alias in testing if pattern unification applies.herbelin
2011-12-04Discarding let-ins from the instances of the evars in theherbelin
2011-11-23Adds a pair of function in Evar_util to gather dependent evars in anaspiwack
2011-11-06Fixing incorrect change to pattern-unification over Meta's introducedherbelin
2011-10-25Continuing r14585 (ill-typed restriction bug).herbelin
2011-10-25Continuing r1492 (useless changes were inadvertantly committed)herbelin
2011-10-25New strategy to infer return predicate of match construct whenherbelin
2011-10-24Fixing another bug revealing ill-typed use of evar restriction.herbelin
2011-10-24Fixing instance/filter mismatch in materialize_evar + documentation.herbelin
2011-10-17Partly reverting r14539 about fully expanding "let-in"s and not justherbelin
2011-10-10More robust and uniform treatment of aliases in evarutil.mlherbelin
2011-10-10Applied the trick of Chung-Kil Hur to solve second-order matchingherbelin
2011-10-10Fixing buggy abberant code for Evarutil.expand_evarherbelin
2011-10-10Passed conv_algo to evar_define and move call to solve_refl toherbelin
2011-08-03Fix nf_evars_undefinedmsozeau
2011-07-29Evarutil: replace generic list_distinct on constr by constr_list_distinctpuech
2011-07-29Evarutil: replaced some generic = on constr by destructorspuech
2011-07-29Evarutil: generic equality on constr replaced by destructorspuech
2011-07-29Evarutil: generic equality on constr replaced by eq_constr (x2)puech
2011-07-29Evarutil: generic equality on constr replaced by eq_constrpuech
2011-06-13Added full pattern-unification on Meta for tactic unification.herbelin
2011-06-10Fixes in pruning, do not fail if pruning is impossible due to typing constrai...msozeau
2011-06-09More fixes in pruning/restriction of evars during unification.msozeau
2011-06-08Fixes in pruning in unification.msozeau
2011-06-07- Fix restrict_hyps to not allow filtering on a variable required to typechec...msozeau
2011-04-13- Make typeclass transparency information directly availablemsozeau
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-02 06:47:23 +0000