coq - The formal proof system

Age	Commit message (Expand)	Author
2014-11-04	Experimentally applying eager evar substitution at the same time as	Hugo Herbelin
2014-11-04	test suite: some reproduction cases for recently-reported bugs.	Xavier Clerc
2014-11-04	Test for bug #2149.	Pierre-Marie Pédrot
2014-11-03	Writing rename_hyps in the new monad.	Pierre-Marie Pédrot
2014-11-03	New bugs revealed fixed: #3408 by (probably) Maxime's commits	Hugo Herbelin
2014-11-03	Now that evars can be parsed, protect strongly Check from calling kernel with...	Hugo Herbelin
2014-11-03	Fixing confused code for interpretations of evar instances.	Hugo Herbelin
2014-11-03	vernac_classifier: VernacDeclareTacticDefinition does not alter the parser	Enrico Tassi
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