coq - The formal proof system

Age	Commit message (Expand)	Author
2009-11-16	Taking advantage of the new "Include Self Type" in DecidableType2 and NZAxioms	letouzey
2009-11-16	Include Self (Type) Foo: applying a (Type) Functor to the current context	letouzey
2009-11-16	Some lemmas about dependent choice + extensions of Compare_dec +	herbelin
2009-11-15	Fix type class discharge again.	msozeau
2009-11-15	Document Generalizable Variables, and change syntax to	msozeau
2009-11-15	Fix [Instance: forall ..., C args := t] declarations to behave as	msozeau
2009-11-13	Move Obj.magic call to the Vm module	glondu
2009-11-13	Remove dubious call to Obj.magic (and dead code, by the way)	glondu
2009-11-13	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-12	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-11	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-10	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-09	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-08	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-06	- Fix discharge bug in typeclasses: some constrs were not actually	msozeau