coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Substitute terms for evars-as-goals as soon as they are solved in	msozeau	2009-11-27
*	svn:ignore property	herbelin	2009-11-26
*	Fixing xml theory file export (was not consistent with coqdoc file	herbelin	2009-11-26
*	Fix for notation scope & inductive types	vsiles	2009-11-25
*	Minor fixes in typeclasses, avoiding repeated evar normalizations.	msozeau	2009-11-24
*	Small extra result on JMeq vs eq_dep.	herbelin	2009-11-24
*	Ergonomy and robustness fix	vgross	2009-11-23
*	Lazier behaviour of [auto] when introducing hypothesis: query the hint db's o...	puech	2009-11-21
*	Refactoring of coqide backtrack code, with the intent to put everything	vgross	2009-11-19
*	Correction du bug #2118 (Coqdep does not escape #)	notin	2009-11-19
*	Now "Include Self <expr>" handles partially applied functors, cf for example ...	soubiran	2009-11-18
*	Diamond-shape instead of linear hiearchy in Numbers/NatInt	letouzey	2009-11-18
*	Allow interactive proofs in module types	letouzey	2009-11-18
*	Module subtyping : allow many <: and module type declaration with <:	letouzey	2009-11-18
*	New syntax <+ for chains of Include (or Include Type) (or Include Self (Type))	letouzey	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-16
*	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-15
*	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-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