index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
pretyping
/
evarutil.ml
Commit message (
Expand
)
Author
Age
*
More cleaning
ppedrot
2012-06-01
*
Evar_kinds.mli containing former Evd.hole_kind, avoid deps on Evd
letouzey
2012-05-29
*
Corrects a bug in the refine tactic which could drop evar bodies.
aspiwack
2012-04-18
*
Fixing a "Not_Found" bug related to commit 15061 on the use of evar candidates.
herbelin
2012-04-16
*
Speedup free_vars_and_rels_up_alias_expansion (evarconv)
gareuselesinge
2012-04-05
*
Unification: Fixing bug in materialize_evar (spotted by MathClasses).
herbelin
2012-03-26
*
Unification: Added a heuristic to solve problems of the form
herbelin
2012-03-26
*
Little bug in r15061 leading to unusable debug mode.
herbelin
2012-03-23
*
Use a careful analysis of dependencies in restricting instances to
herbelin
2012-03-20
*
Unification: when matching "?n[...,(C u1..un),...] = C u1..un" keep a
herbelin
2012-03-20
*
Generalized the use of evar candidates in type inference unification:
herbelin
2012-03-20
*
Reorganizing the structure of evarutil.ml (only restructuration, no
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
*
Fix in evarutil: add a conversion problem for ?x ts = ?x us only if ts and us...
msozeau
2012-02-15
*
Type inference unification: fixed a 8.4 bug in the presence of unification
herbelin
2012-01-04
*
Introducing a notion of evar candidates to be used when an evar is
herbelin
2011-12-16
*
Registering universe and meta/evar counters as summaries so as to
herbelin
2011-12-05
*
Yet another fix about alias in testing if pattern unification applies.
herbelin
2011-12-05
*
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 r14585 (ill-typed restriction bug).
herbelin
2011-10-25
*
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
*
Fixing another bug revealing ill-typed use of evar restriction.
herbelin
2011-10-24
*
Fixing instance/filter mismatch in materialize_evar + documentation.
herbelin
2011-10-24
*
Partly reverting r14539 about fully expanding "let-in"s and not just
herbelin
2011-10-17
*
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
*
Fixing buggy abberant code for Evarutil.expand_evar
herbelin
2011-10-10
*
Passed conv_algo to evar_define and move call to solve_refl to
herbelin
2011-10-10
*
Fix nf_evars_undefined
msozeau
2011-08-03
*
Evarutil: replace generic list_distinct on constr by constr_list_distinct
puech
2011-07-29
*
Evarutil: replaced some generic = on constr by destructors
puech
2011-07-29
*
Evarutil: generic equality on constr replaced by destructors
puech
2011-07-29
*
Evarutil: generic equality on constr replaced by eq_constr (x2)
puech
2011-07-29
*
Evarutil: generic equality on constr replaced by eq_constr
puech
2011-07-29
*
Added full pattern-unification on Meta for tactic unification.
herbelin
2011-06-13
*
Fixes in pruning, do not fail if pruning is impossible due to typing constrai...
msozeau
2011-06-10
*
More fixes in pruning/restriction of evars during unification.
msozeau
2011-06-09
*
Fixes in pruning in unification.
msozeau
2011-06-08
*
- Fix restrict_hyps to not allow filtering on a variable required to typechec...
msozeau
2011-06-07
*
- Make typeclass transparency information directly available
msozeau
2011-04-13
*
- Remove create_evar_defs
msozeau
2011-04-13
*
Catch NotArity exception and transform it into an anomaly in retyping.
msozeau
2011-04-11
*
- Fix solve_simpl_eqn which was cheking instances types in the wrong environm...
msozeau
2011-03-23
*
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
[next]