coq - The formal proof system

Age	Commit message (Expand)	Author
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
2014-10-27	Removing an Evd.merge in Newring.	Pierre-Marie Pédrot
2014-10-27	Fixes for PG (Close 3763, 3770)	Enrico Tassi
2014-10-27	Make sure that Logic/ExtensionalityFacts gets compiled.	Guillaume Melquiond
2014-10-27	Fix some typos.	Guillaume Melquiond
2014-10-27	Use the url package, since coqdoc generates \url commands.	Guillaume Melquiond
2014-10-27	Making destruct on idents with maximal implicit arguments working, by	Hugo Herbelin
2014-10-27	Ensuring compatibility when an hypothesis used for destruct is	Hugo Herbelin
2014-10-27	Fixing evars lost in interpretation of eliminator of destruct.	Hugo Herbelin
2014-10-27	Fixing clash in test destruct.v.	Hugo Herbelin
2014-10-27	Dead code	Hugo Herbelin
2014-10-27	Fix some typos in comments.	Guillaume Melquiond
2014-10-26	Preventing potential evar leak in Rewrite.	Pierre-Marie Pédrot
2014-10-26	Applying like-first selection for destruct in hypotheses.	Hugo Herbelin
2014-10-26	Fixing destruct/induction with a using clause on a non-inductive type,	Hugo Herbelin
2014-10-26	Dead code + typo.	Hugo Herbelin
2014-10-25	Changed implementation of lib/heap.ml to use Braun trees	Jean-Christophe Filliatre
2014-10-25	This commit introduces changes in induction and destruct.	Hugo Herbelin
2014-10-25	VarInstance are also goals.	Hugo Herbelin