coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	"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
*	Fix in evarutil: add a conversion problem for ?x ts = ?x us only if ts and us...	msozeau	2012-02-15
*	In [reflexivity], [symmetry] etc, use the type found by looking at the relati...	msozeau	2012-02-14
*	- Fix dependency computation in eterm to not consider filtered variables.	msozeau	2012-02-14
*	Arguments supports extra notation scopes	gareuselesinge	2012-02-14
*	Additional comment on Focus Conditions.	aspiwack	2012-02-07
*	Documentation for Grab Existential Variables.	aspiwack	2012-02-07
*	A "Grab Existential Variables" to transform the unresolved evars at the end o...	aspiwack	2012-02-07
*	Typo in comments.	aspiwack	2012-02-07
*	correcting inversion in list of generated tcc of Function	letouzey	2012-02-03
*	More information returned by coqtop about its internal state. Hopefully we'll...	ppedrot	2012-02-02
*	Fix unblocking code in dependent destruction due to zeta being used in unfold...	msozeau	2012-02-01
*	Corrected a careless cut-and-paste in Gallina description which dated back to...	ppedrot	2012-02-01
*	Debugger vs tracer: Two different behaviors wrt printing: The debugger	herbelin	2012-02-01
*	Improved synchronisation of stdlib index page with current library state.	herbelin	2012-02-01
*	Revert "Tentative to fix bug #2628 by not letting intuition break records. Mi...	msozeau	2012-01-31
*	index-list.html.template: add missing files	pboutill	2012-01-31
*	Fix consequence of pp bugfix in testsuite	pboutill	2012-01-31
*	Makefile.build: add targets install-devfiles and install-ide-devfiles	pboutill	2012-01-31
*	Bug #2041: unfold at betaiotaZETA normalize like unfold	pboutill	2012-01-31
*	Fix camlp4 compilation	pboutill	2012-01-31
*	Added an pattern / occurence syntax for vm_compute.	ppedrot	2012-01-30
*	Tentative to fix bug #2628 by not letting intuition break records. Might be t...	msozeau	2012-01-28