coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Univ: enforce_leq instead of enforce_geq for more uniformity	letouzey	2012-03-22
*	Univ: switch the order of int and dir_path in UniverseLevel.Level	letouzey	2012-03-22
*	Update of .gitignore (via a regexp g_*.ml)	letouzey	2012-03-22
*	evarconv: MaybeFlex/MaybeFlex case infers more Canonical Structures	gareuselesinge	2012-03-22
*	Ppvernac: nicer printing of proof delimiters { ... }	letouzey	2012-03-21
*	Pfedit: avoid Undoing too much	letouzey	2012-03-21
*	Fix interface of resolve_typeclasses: onlyargs -> with_goals:	msozeau	2012-03-20
*	Arranged for the desirable behaviour that bullets do not see beyond braces.	aspiwack	2012-03-20
*	Fixing bug #2724 (using notations with binders in cases patterns	herbelin	2012-03-20
*	Fixing alpha-conversion bug #2723 introduced in r12485-12486.	herbelin	2012-03-20
*	Continuing r15045-15046 and r15055 (fixing bug #2732 about atomic	herbelin	2012-03-20
*	Use a careful analysis of dependencies in restricting instances to	herbelin	2012-03-20
*	Force Check (which, from 8.4beta, accepts unresolved evars) to however	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
*	Turning proofs of well-ordering of lexicographic product transparent	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
*	Hopefully complying with camlp5 < 6.00 syntax	herbelin	2012-03-19
*	Bug 2709: Duplication in coqdoc index entries	pboutill	2012-03-19
*	RefMan: Environment variables description update	pboutill	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
*	Yet another subtlety with bug 2732: when several grammar rules of a	herbelin	2012-03-18
*	Removing redundant entry int_nelist and removing extra space when	herbelin	2012-03-18
*	Fixing bug #2732 (anomaly when using the tolerance for writing	herbelin	2012-03-18
*	Fix merge and add missing file.	msozeau	2012-03-14
*	Fix merge.	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
*	Final part of moving Program code inside the main code. Adapted add_definitio...	msozeau	2012-03-14
*	Integrated obligations/eterm and program well-founded fixpoint building to to...	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
*	Univ: avoid recording dummy universe constraints u<=u or u=u	letouzey	2012-03-12
*	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
*	Univ: a better Constraint.compare	letouzey	2012-03-01
*	Corrects the erroneous error message when trying to unfocus a fully	aspiwack	2012-03-01
*	Removed a superfluous function in proof.mli. Preparing for incoming	aspiwack	2012-03-01
*	New version of recdef :	jforest	2012-03-01
*	various corrections in invfun due to a modification in induction	jforest	2012-03-01
*	Univ: a faster is_leq test used when possible	letouzey	2012-02-29
*	correcting a little bug in invfun.ml	jforest	2012-02-29