coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
*	Another correction to the dependent existential variable printing	aspiwack	2012-07-10
*	Fixes bug #2678	aspiwack	2012-07-06
*	Added an indirection with respect to Loc in Compat. As many [open Compat]	ppedrot	2012-06-22
*	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