coq - The formal proof system

Age	Commit message (Expand)	Author
2014-11-03	Show: do print the goals	Enrico Tassi
2014-11-03	STM: code refactoring	Enrico Tassi
2014-11-03	Subtle swap of lines to preserve VarInstance src field before checking	Hugo Herbelin
2014-11-03	Fix to 844431761 on improving elimination with indices, getting rid of	Hugo Herbelin
2014-11-03	STM: fix printing of goals when on a tty interface	Enrico Tassi
2014-11-03	Fix error reporting id on VtUnknown commands	Enrico Tassi
2014-11-03	Fixing inefficiency in typeclass resolution.	Pierre-Marie Pédrot
2014-11-02	Saving some nf_evars in the code of destruct/induction.	Hugo Herbelin
2014-11-02	Improving elimination with indices, getting rid of intrusive residual	Hugo Herbelin
2014-11-02	Some reorganization of the code for destruct/induction:	Hugo Herbelin
2014-11-02	Fixing subterm matched for destruct when it is matched from prefix.	Hugo Herbelin
2014-11-02	Supporting "at occs" as a short-hand for "in \|- * at occs" in "destruct".	Hugo Herbelin
2014-11-02	Plural and singular forms in error messages.	Hugo Herbelin
2014-11-02	Cosmetic changes.	Hugo Herbelin
2014-11-02	Fixing 1177da327 (reorganization of the test for generic selection of	Hugo Herbelin
2014-11-02	Fixing file destruct.v.	Hugo Herbelin
2014-11-01	Document [Info] command.	Arnaud Spiwack
2014-11-01	Info: the warning message of the defunct [info] tactic now points to the [Inf...	Arnaud Spiwack
2014-11-01	Info: do not record info trace unless needed.	Arnaud Spiwack
2014-11-01	Add an [Info Level] option to print info traces automatically.	Arnaud Spiwack
2014-11-01	Don't raise an error when printing intro-patterns in [functional induction].	Arnaud Spiwack
2014-11-01	Info: print name of calls to Ltac constants ([TacCall]).	Arnaud Spiwack
2014-11-01	Info: tactic notations (TacAlias) print their names.	Arnaud Spiwack
2014-11-01	Info: Tactics coming from [TACTIC EXTEND] print their names.	Arnaud Spiwack
2014-11-01	Info: print the name of atomic tactics.	Arnaud Spiwack
2014-11-01	Add a interpreted level [tacexpr] to [Tacexpr] together with its printer.	Arnaud Spiwack
2014-11-01	Info: Ltac's idtac logs its message in the info trace.	Arnaud Spiwack
2014-11-01	Info: print a name for the primitive tactics in [Proofview].	Arnaud Spiwack
2014-11-01	Info: dispatching-branches are declared as such in the info trace.	Arnaud Spiwack
2014-11-01	Add [Info] command.	Arnaud Spiwack
2014-11-01	An API for info traces.	Arnaud Spiwack
2014-10-31	Reorganization of the test for generic selection of occurrences in	Hugo Herbelin
2014-10-31	More "open" by default for trace debugging.	Hugo Herbelin
2014-10-31	Enlarge the cases where the like first selection is used in destruct.	Hugo Herbelin
2014-10-31	Listing a few examples of destruct showing unsatisfactory behaviors.	Hugo Herbelin
2014-10-31	Avoid "destruct H" to apply on H itself when H is a section variable.	Hugo Herbelin
2014-10-31	Feedback message: hold extra info to help routing	Enrico Tassi
2014-10-31	STM: new worker for queries	Enrico Tassi
2014-10-31	STM: reorganize code and file names	Enrico Tassi
2014-10-31	Show_script called only if in coqtop mode	Enrico Tassi
2014-10-30	Better error messages when unfreezing summary entries	Enrico Tassi
2014-10-30	Fix backtracking issue in Defined (Close 3780)	Enrico Tassi
2014-10-28	Haskell extraction: use explicit -XMagicHash instead of -fglasgow-exts	Nickolai Zeldovich
2014-10-28	Haskell extraction: put unsafeCoerce type declaration later	Nickolai Zeldovich
2014-10-28	Allow camlp5 to have version numbers like "6.09-exp"	jbapple
2014-10-27	Cleaning and documenting Clenv.make_evar_clause	Pierre-Marie Pédrot
2014-10-27	Removing dead code from Evd.	Pierre-Marie Pédrot
2014-10-27	Removing the Evd.diff function.	Pierre-Marie Pédrot
2014-10-27	Removing the last Evd.diff from Hints.	Pierre-Marie Pédrot
2014-10-27	Removing the Evd.merge function.	Pierre-Marie Pédrot