coq - The formal proof system

Age	Commit message (Expand)	Author
2012-03-23	Documentation of last commit concerning Backtracking	letouzey
2012-03-23	A unified backtrack mechanism, with a basic "Show Script" as side-effect	letouzey
2012-03-23	Remove undocumented command "Delete foo"	letouzey
2012-03-23	Remove old proof-managment commands Suspend/Resume	letouzey
2012-03-23	Little bug in r15061 leading to unusable debug mode.	herbelin
2012-03-22	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-21	Ppvernac: nicer printing of proof delimiters { ... }	letouzey
2012-03-21	Pfedit: avoid Undoing too much	letouzey
2012-03-20	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-19	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-18	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-14	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-13	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-12	Univ: avoid recording dummy universe constraints u<=u or u=u	letouzey
2012-03-02	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-01	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