coq - The formal proof system

Age	Commit message (Expand)	Author
2014-11-20	Re-removing the Hiddentac module. For some reason it had been reintroduced	Pierre-Marie Pédrot
2014-11-20	Global.env chasing in Inv.	Pierre-Marie Pédrot
2014-11-20	Adding locations to tclZEROMSG.	Pierre-Marie Pédrot
2014-11-20	Setting printing flags on the printing of mutual inductives.	Pierre-Marie Pédrot
2014-11-20	Moving mutual inductive printing from Printer to Printmod.	Pierre-Marie Pédrot
2014-11-19	Making map_union a standard function of the ML library.	Hugo Herbelin
2014-11-19	Slightly improving error messages when mismatch with Proof using at Qed time.	Hugo Herbelin
2014-11-19	Option -type-in-type continued (deactivate test for inferred sort of	Hugo Herbelin
2014-11-19	Continuing fixing nested but convertible occurrences in find_subterm	Hugo Herbelin
2014-11-19	Print [uconstr] in genargs.	Arnaud Spiwack
2014-11-19	Print [uconstr]-s in [idtac] messages.	Arnaud Spiwack
2014-11-19	Proper printer for [uconstr] in [Pptactic].	Arnaud Spiwack
2014-11-19	Printing function for [uconstr].	Arnaud Spiwack
2014-11-19	uconstr: fix bug in interpretation of Ltac-bound name in let-tuple and patter...	Arnaud Spiwack
2014-11-19	Glob-ops: a name-mapping operation for pattern-matching binders.	Arnaud Spiwack
2014-11-19	Adding rich-printing facilities to Printmod.	Pierre-Marie Pédrot
2014-11-18	Tentative rephrasing of error message for rewrite.	Hugo Herbelin
2014-11-18	Hopefully the last word on having "simpl f" complying with the	Hugo Herbelin
2014-11-18	Fixing a little bug with nested but convertible occurrences in "destruct at".	Hugo Herbelin
2014-11-18	Fixing detection of occurrences in the presence of nested subterms for	Hugo Herbelin
2014-11-18	Clarifying the role of ListSet.v in the library, compared to other	Hugo Herbelin
2014-11-17	Adding notation terminals to coqtop highlight.	Pierre-Marie Pédrot
2014-11-17	Fixing semantics of Ppconstr.print_hunks.	Pierre-Marie Pédrot
2014-11-17	Missing keywords in Ppconstr.	Pierre-Marie Pédrot
2014-11-17	Setting printing tags for Ltac.	Pierre-Marie Pédrot
2014-11-17	Moving printing code for red_expr and may_eval to Pptactic.	Pierre-Marie Pédrot
2014-11-17	Documenting the -color option.	Pierre-Marie Pédrot
2014-11-17	Documenting use of colors in Coq.	Pierre-Marie Pédrot
2014-11-17	Default styles for printing tags.	Pierre-Marie Pédrot
2014-11-17	Setting error tag on generic errors returned by Coqtop.	Pierre-Marie Pédrot
2014-11-16	Enforcing a stronger difference between the two syntaxes "simpl	Hugo Herbelin
2014-11-16	Fixing side bug in db37c9f3f32ae7 delaying interpretation of the	Hugo Herbelin
2014-11-16	For consistency with other coqtop flags, use -help rather than --help in usage.	Hugo Herbelin
2014-11-15	Adding tags to messages.	Pierre-Marie Pédrot
2014-11-15	Removing a pperrnl.	Pierre-Marie Pédrot
2014-11-15	Adding a command line option to print out accepted color tags.	Pierre-Marie Pédrot
2014-11-15	Additional style tags for constrs.	Pierre-Marie Pédrot
2014-11-15	Reworking the -color flag of coqtop.	Pierre-Marie Pédrot
2014-11-15	Removing deprecated code handling color in Pp.	Pierre-Marie Pédrot
2014-11-15	Setting a keyword tag in Ppconstr.	Pierre-Marie Pédrot
2014-11-15	Plugging the color initialization in the Coqtop loop.	Pierre-Marie Pédrot
2014-11-15	Adding a pretty-printing style library.	Pierre-Marie Pédrot
2014-11-15	Adding a terminal library.	Pierre-Marie Pédrot
2014-11-14	Use return code to classify anomalies as active open bugs.	Xavier Clerc
2014-11-14	Exit with code 129 when an anomaly occurs.	Xavier Clerc
2014-11-14	Get rif of exit codes 120, 121, 123, and 124.	Xavier Clerc
2014-11-14	Add missing "Fail" to test case for bug #2814.	Xavier Clerc
2014-11-14	Reproduction cases for the test suite.	Xavier Clerc
2014-11-14	Preserving the good effect of 014e5ac92a on not leaving dangling local	Hugo Herbelin
2014-11-13	Fixing Scheme Equality, after bug introduced in bf018569405c.	Hugo Herbelin