coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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
*	correction of bug 2457	jforest	2012-02-29
*	Fix compilation of Constrintern...	pboutill	2012-02-29
*	RefMan update about match syntax.	pboutill	2012-02-29
*	In the syntax of pattern matching, the arguments of the inductive in the "in"	pboutill	2012-02-29
*	In the syntax of pattern matching, "in" clauses are patterns.	pboutill	2012-02-29
*	Vector: missing injection lemmas and better impossible branches	pboutill	2012-02-29
*	Bug 2703: send stdout dump to coqide when an error occurs.	pboutill	2012-02-29
*	Coq_makefile: Add of extra options by default	pboutill	2012-02-29
*	Univ: correct compare_neq (fix #2703)	letouzey	2012-02-27
*	Implement the substitution function for global options. Fixes anomaly in ssre...	msozeau	2012-02-23
*	Ide: sentences found by find_phrase_starting_at should be nonempty (fix #2683)	letouzey	2012-02-22
*	Use a heuristic to not simplify equality hypotheses remaining after dependent...	msozeau	2012-02-20
*	- changing minimal version for OCaml: Coq uses Filename.dirsep that is availa...	notin	2012-02-20
*	Correct application of head reduction.	msozeau	2012-02-20
*	Document the [unify] tactic.	msozeau	2012-02-18
*	Fix handling of space after "Notation" or "where", add missing keywords.	msozeau	2012-02-16
*	Avoid retrying uncessarily to prove independent remaining obligations in Prog...	msozeau	2012-02-15
*	Avoid unnecessary normalizations w.r.t. evars in Program.	msozeau	2012-02-15