coq - The formal proof system

Age	Commit message (Expand)	Author
2009-11-27	Substitute terms for evars-as-goals as soon as they are solved in	msozeau
2009-11-26	svn:ignore property	herbelin
2009-11-26	Fixing xml theory file export (was not consistent with coqdoc file	herbelin
2009-11-25	Fix for notation scope & inductive types	vsiles
2009-11-24	Minor fixes in typeclasses, avoiding repeated evar normalizations.	msozeau
2009-11-24	Small extra result on JMeq vs eq_dep.	herbelin
2009-11-23	Ergonomy and robustness fix	vgross
2009-11-21	Lazier behaviour of [auto] when introducing hypothesis: query the hint db's o...	puech
2009-11-19	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-18	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-16	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-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