coq - The formal proof system

Age	Commit message (Expand)	Author
2015-05-05	Merge branch 'v8.5'	Pierre-Marie Pédrot
2015-05-04	Add a [Redirect] vernacular command	Clément Pit--Claudel
2015-04-23	Remove almost all the uses of string concatenation when building error messages.	Guillaume Melquiond
2015-04-09	Merge branch 'v8.5' into trunk	Pierre Letouzey
2015-03-31	Declarative mode: plug the specialised printers back.	Arnaud Spiwack
2015-03-31	Better formatting of messages in proofs.	Arnaud Spiwack
2015-03-31	Generalisation of the "end command" argument of the goal printer.	Arnaud Spiwack
2015-03-30	Merge branch 'v8.5' into trunk	Enrico Tassi
2015-03-27	Putting the From parameter of the Require command into the AST.	Pierre-Marie Pédrot
2015-03-13	rewiring Czar printers that were disabled	Pierre Corbineau
2015-03-11	Merge branch 'v8.5'	Pierre-Marie Pédrot
2015-03-09	Do not display the status of monomorphic constants unless in universe-polymor...	Guillaume Melquiond
2015-03-02	rewiring Czar printers that were disabled	Pierre Corbineau
2015-02-23	Merge branch 'v8.5'	Pierre-Marie Pédrot
2015-02-21	Better English for #4070 implicit arguments message (thanks to Jason for his ...	Hugo Herbelin
2015-02-20	An answer to #4070 (message for implicit arguments of inl not clear).	Hugo Herbelin
2015-02-15	Merge branch 'v8.5'	Pierre-Marie Pédrot
2015-02-14	Abstract: "Qed export ident, .., ident" to preserve v8.4 behavior	Enrico Tassi
2015-02-10	Merge branch 'v8.5'	Pierre-Marie Pédrot
2015-02-06	More efficient Richpp.	Pierre-Marie Pédrot
2015-02-02	Removing dead code.	Pierre-Marie Pédrot
2015-01-25	Merge branch 'v8.5' into trunk.	Pierre-Marie Pédrot
2015-01-24	Isolate a function for printing evar sets.	Hugo Herbelin
2015-01-23	Splitting ML tactics in one function per grammar entry.	Pierre-Marie Pédrot
2015-01-21	Embedding the index of the ML tactic entry in the Tacexpr AST.	Pierre-Marie Pédrot
2015-01-18	Univs: proper printing of global and local universe names (only	Matthieu Sozeau
2015-01-17	Univs: proper printing of global and local universe names (only	Matthieu Sozeau
2015-01-13	Fix issue in printing due to de Bruijn bug when constructing compatibility	Matthieu Sozeau
2015-01-12	Update headers.	Maxime Dénès
2015-01-11	Declarations.mli refactoring: module_type_body = module_body	Pierre Letouzey
2015-01-08	Continuing 785f82ee1 on reverting not only f5d7b2b1e but also	Hugo Herbelin
2015-01-08	Fixed and extend bullet related info/error messages. + doc.	Pierre Courtieu
2014-12-27	Revert "Term: include a function to print terms"	Enrico Tassi
2014-12-26	Term: include a function to print terms	Enrico Tassi
2014-12-23	A global [gfail] tactic which works like [fail] except that it fails even if ...	Arnaud Spiwack
2014-12-23	Fix compilation error in some configurations.	Arnaud Spiwack
2014-12-19	Add a backtracking version of Ltac's [match].	Arnaud Spiwack
2014-12-18	Proof using: New vernacular to name sets of section variables	Enrico Tassi
2014-12-18	Fixed bad newlines in output for std output and emacs.	Pierre Courtieu
2014-12-16	msg_info now puts infomsg tag in emacs mode.	Pierre Courtieu
2014-12-15	Changed bullet informations to warning for better display in PG.	Pierre Courtieu
2014-12-15	About now accepts hypothesis names and goal selector.	Pierre Courtieu
2014-12-12	Add Ltac syntax for the [tclIFCATCH] primitive.	Arnaud Spiwack
2014-12-12	Extend the syntax of simpl with a delta flag.	Arnaud Spiwack
2014-12-12	Searchxxx now search also the hypothesis and support goal selector.	Pierre Courtieu
2014-12-04	Improving error message when one instance-hole is not found.	Hugo Herbelin
2014-11-30	Fixing printing of dirpathes in Ppconstr. It was reversed.	Pierre-Marie Pédrot
2014-11-25	Adding tag output to references in Ppconstr.	Pierre-Marie Pédrot
2014-11-24	Plugging console highlighting in for toplevel and compilation error messages.	Pierre-Marie Pédrot
2014-11-22	Removing useless flag of the historical move tactic.	Pierre-Marie Pédrot