coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Remove useless call to Obj.magic	glondu	2009-11-13
*	Make usages of the Obj module explicit	glondu	2009-11-13
*	Remove useless ppevd (which is identical to ppevm)	glondu	2009-11-13
*	scripting area now grabs focus at startup.	vgross	2009-11-13
*	new handling for lexical structures.	vgross	2009-11-13
*	lexing refactoring	vgross	2009-11-13
*	the inlining computation at functor application was raising not_found when th...	soubiran	2009-11-13
*	Fix test-suite scripts: [Generalizable Variables] and small	msozeau	2009-11-13
*	Backtrack on fixing #2167	herbelin	2009-11-12
*	Suppression de l'appel à Lexing.new_line (qui n'existe pas dans les versions...	notin	2009-11-12
*	Oops, nf_evar_defs just changed to nf_evar_map.	msozeau	2009-11-12
*	Don't forget to normalize everything w.r.t. evars (fixes bug #2103).	msozeau	2009-11-12
*	Restore test-suite/csdp.cache erased from svn by mistake	letouzey	2009-11-12
*	BigQ / BigN / BigZ syntax and scope improvements (sequel to 12504)	letouzey	2009-11-12
*	Experiment propagation of implicit arguments and arguments scope for	herbelin	2009-11-12
*	Addendum to revision 12501.	herbelin	2009-11-12
*	Repair interpretation of numeral for BigQ, add a printer (close #2160)	letouzey	2009-11-12
*	Better compatibility for Peqb	letouzey	2009-11-11
*	Promote evar_defs to evar_map (in Evd)	glondu	2009-11-11
*	Backtracking on the use of automatically generated schemes for	herbelin	2009-11-11
*	Added support for multiple where-clauses in Inductive and co (see wish #2163).	herbelin	2009-11-11
*	Redoing broken commit r12498 (fixing bug #2167 + attempt to test the	herbelin	2009-11-11
*	Fixing bug #2167 + attempt to test the compatibility of a more robust	herbelin	2009-11-11
*	Test for bug #2168, forgotten in r12496.	herbelin	2009-11-11
*	Fixed bug #2168 (closing a section may have as side-effect the erasure	herbelin	2009-11-11
*	Improving abbreviations/notations + backtrack of semantic change in r12439	herbelin	2009-11-11
*	Compatibility ocaml <= 3.09	herbelin	2009-11-10
*	Correction du bug #2183	notin	2009-11-10
*	use only why-dp, support for z3	marche	2009-11-10
*	SpecViaZ.NSig: all-in-one spec for [pred] and [sub] based on ZMax	letouzey	2009-11-10
*	Simplification of Numbers, mainly thanks to Include	letouzey	2009-11-10
*	DecidableType: A specification via boolean equality as an alternative to eq_dec	letouzey	2009-11-10
*	Deactivation of (intrusive) printing of abbreviations from non-imported modules.	herbelin	2009-11-09
*	Commit 12485 continued.	herbelin	2009-11-09
*	A bit of cleaning around name generation + creation of dedicated file namegen.ml	herbelin	2009-11-09
*	Quick fix for restoring a left-to-right rewriting lemma compatible	herbelin	2009-11-09
*	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12483 85f007b7-540e-0...	fbesson	2009-11-09
*	Fixed "Scheme Equality" when another instance of the scheme on the	herbelin	2009-11-08
*	Restructuration of command.ml + generic infrastructure for inductive schemes	herbelin	2009-11-08
*	Took local definitions into account in the test for deciding whether	herbelin	2009-11-08
*	Use generalizable variables info when internalizing arbitrary bindings,	msozeau	2009-11-08
*	- Fix discharge bug in typeclasses: some constrs were not actually	msozeau	2009-11-06
*	Datatypes.length and app defined back via fun+fix instead of Fixpoint	letouzey	2009-11-06
*	Numbers: finish files NStrongRec and NDefOps	letouzey	2009-11-06
*	Numbers: more (syntactic) changes toward new style of type classes	letouzey	2009-11-06
*	Misc fixes.	msozeau	2009-11-06
*	Changement de la version minimale requise de OCaml (3.07 => 3.09.3).	notin	2009-11-05
*	Correction du bug #2142	notin	2009-11-05
*	Correction du bug #2153 (-D n'est pas une option standard de install)	notin	2009-11-05
*	Fixed record syntax "{\|x=...; y=...\|}" so that it works with qualified names.	gmelquio	2009-11-04