coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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
*	Univ: enforce_leq instead of enforce_geq for more uniformity	letouzey	2012-03-22
*	evarconv: MaybeFlex/MaybeFlex case infers more Canonical Structures	gareuselesinge	2012-03-22
*	Fix interface of resolve_typeclasses: onlyargs -> with_goals:	msozeau	2012-03-20
*	Fixing alpha-conversion bug #2723 introduced in r12485-12486.	herbelin	2012-03-20
*	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
*	More adaptations of pretyping/coercion to Program mode.	msozeau	2012-03-19
*	Fix bugs related to Program integration.	msozeau	2012-03-19
*	Fixes bug: #2692 (Arguments/simpl off by 1)	gareuselesinge	2012-03-19
*	Arguments/simpl: allow ! even on non fixpoints	gareuselesinge	2012-03-19
*	Fix merge and add missing file.	msozeau	2012-03-14
*	Revise API of understand_ltac to be parameterized by a flag for resolution of...	msozeau	2012-03-14
*	Merge fixes	msozeau	2012-03-14
*	Everything compiles again.	msozeau	2012-03-14
*	Second step of integration of Program:	msozeau	2012-03-14
*	Remove support for "abstract typing constraints" that requires unicity of sol...	msozeau	2012-03-14
*	A bit of cleaning: unifying push_rels and push_rel_context.	herbelin	2012-03-13
*	Fixing vm_compute bug #2729 (function used to decompose constructors	herbelin	2012-03-13
*	Glob_term.predicate_pattern: No number of parameters with letins.	pboutill	2012-03-02
*	"Let in" in pattern hell, one more iteration	pboutill	2012-03-02
*	Noise for nothing	pboutill	2012-03-02
*	Univ: a univ_depends function to avoid a hack in Inductiveops	letouzey	2012-03-01
*	Fix in evarutil: add a conversion problem for ?x ts = ?x us only if ts and us...	msozeau	2012-02-15
*	Bug #2041: unfold at betaiotaZETA normalize like unfold	pboutill	2012-01-31
*	Added an pattern / occurence syntax for vm_compute.	ppedrot	2012-01-30
*	Printing bugs with match patterns:	herbelin	2012-01-27
*	Fix for Program Instance not separately checking the resolution of evars of t...	msozeau	2012-01-23
*	Inductiveops.nb_*{,_env} cleaning	pboutill	2012-01-16
*	Type inference unification: fixed a 8.4 bug in the presence of unification	herbelin	2012-01-04
*	Granted legitimate wish #2607 (not exposing crude fixpoint body of	herbelin	2011-12-18
*	Continuing 14812 and 14813 (use type information to reduce the	herbelin	2011-12-18
*	Added a flag to control the use of typing when instantiating applied	herbelin	2011-12-17
*	Added ability to take the type of applied metas into account when	herbelin	2011-12-17
*	Reorganizing Unification.unify_0 so as to more easily share code	herbelin	2011-12-17
*	A pass on warning printings. Made systematic the use of msg_warning so	herbelin	2011-12-17
*	Introducing a notion of evar candidates to be used when an evar is	herbelin	2011-12-16
*	Fixing a bug of commit r13310 (activating coercions only when module	herbelin	2011-12-07
*	Backtrack on synchronizing universe counter with reset	herbelin	2011-12-06
*	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
*	Fixed a small regression in pattern-matching compilation introduced in	herbelin	2011-12-04
*	Discarding let-ins from the instances of the evars in the	herbelin	2011-12-04
*	Finally used typing to decide whether an alias needs to be expanded or	herbelin	2011-11-28
*	Fixing dependencies postprocessing bug in pattern-matching compilation.	herbelin	2011-11-28