aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* Supporting "at occs" as a short-hand for "in |- * at occs" in "destruct".Gravatar Hugo Herbelin2014-11-02
* Plural and singular forms in error messages.Gravatar Hugo Herbelin2014-11-02
* Cosmetic changes.Gravatar Hugo Herbelin2014-11-02
* Fixing 1177da327 (reorganization of the test for generic selection ofGravatar Hugo Herbelin2014-11-02
* Fixing file destruct.v.Gravatar Hugo Herbelin2014-11-02
* Document [Info] command.Gravatar Arnaud Spiwack2014-11-01
* Info: the warning message of the defunct [info] tactic now points to the [Inf...Gravatar Arnaud Spiwack2014-11-01
* Info: do not record info trace unless needed.Gravatar Arnaud Spiwack2014-11-01
* Add an [Info Level] option to print info traces automatically.Gravatar Arnaud Spiwack2014-11-01
* Don't raise an error when printing intro-patterns in [functional induction].Gravatar Arnaud Spiwack2014-11-01
* Info: print name of calls to Ltac constants ([TacCall]).Gravatar Arnaud Spiwack2014-11-01
* Info: tactic notations (TacAlias) print their names.Gravatar Arnaud Spiwack2014-11-01
* Info: Tactics coming from [TACTIC EXTEND] print their names.Gravatar Arnaud Spiwack2014-11-01
* Info: print the name of atomic tactics.Gravatar Arnaud Spiwack2014-11-01
* Add a interpreted level [tacexpr] to [Tacexpr] together with its printer.Gravatar Arnaud Spiwack2014-11-01
* Info: Ltac's idtac logs its message in the info trace.Gravatar Arnaud Spiwack2014-11-01
* Info: print a name for the primitive tactics in [Proofview].Gravatar Arnaud Spiwack2014-11-01
* Info: dispatching-branches are declared as such in the info trace.Gravatar Arnaud Spiwack2014-11-01
* Add [Info] command.Gravatar Arnaud Spiwack2014-11-01
* An API for info traces.Gravatar Arnaud Spiwack2014-11-01
* Reorganization of the test for generic selection of occurrences inGravatar Hugo Herbelin2014-10-31
* More "open" by default for trace debugging.Gravatar Hugo Herbelin2014-10-31
* Enlarge the cases where the like first selection is used in destruct.Gravatar Hugo Herbelin2014-10-31
* Listing a few examples of destruct showing unsatisfactory behaviors.Gravatar Hugo Herbelin2014-10-31
* Avoid "destruct H" to apply on H itself when H is a section variable.Gravatar Hugo Herbelin2014-10-31
* Feedback message: hold extra info to help routingGravatar Enrico Tassi2014-10-31
* STM: new worker for queriesGravatar Enrico Tassi2014-10-31
* STM: reorganize code and file namesGravatar Enrico Tassi2014-10-31
* Show_script called only if in coqtop modeGravatar Enrico Tassi2014-10-31
* Better error messages when unfreezing summary entriesGravatar Enrico Tassi2014-10-30
* Fix backtracking issue in Defined (Close 3780)Gravatar Enrico Tassi2014-10-30
* Haskell extraction: use explicit -XMagicHash instead of -fglasgow-extsGravatar Nickolai Zeldovich2014-10-28
* Haskell extraction: put unsafeCoerce type declaration laterGravatar Nickolai Zeldovich2014-10-28
* Allow camlp5 to have version numbers like "6.09-exp"Gravatar jbapple2014-10-28
* Cleaning and documenting Clenv.make_evar_clauseGravatar Pierre-Marie Pédrot2014-10-27
* Removing dead code from Evd.Gravatar Pierre-Marie Pédrot2014-10-27
* Removing the Evd.diff function.Gravatar Pierre-Marie Pédrot2014-10-27
* Removing the last Evd.diff from Hints.Gravatar Pierre-Marie Pédrot2014-10-27
* Removing the Evd.merge function.Gravatar Pierre-Marie Pédrot2014-10-27
* Removing an Evd.merge in Newring.Gravatar Pierre-Marie Pédrot2014-10-27
* Fixes for PG (Close 3763, 3770)Gravatar Enrico Tassi2014-10-27
* Make sure that Logic/ExtensionalityFacts gets compiled.Gravatar Guillaume Melquiond2014-10-27
* Fix some typos.Gravatar Guillaume Melquiond2014-10-27
* Use the url package, since coqdoc generates \url commands.Gravatar Guillaume Melquiond2014-10-27
* Making destruct on idents with maximal implicit arguments working, byGravatar Hugo Herbelin2014-10-27
* Ensuring compatibility when an hypothesis used for destruct isGravatar Hugo Herbelin2014-10-27
* Fixing evars lost in interpretation of eliminator of destruct.Gravatar Hugo Herbelin2014-10-27
* Fixing clash in test destruct.v.Gravatar Hugo Herbelin2014-10-27
* Dead codeGravatar Hugo Herbelin2014-10-27
* Fix some typos in comments.Gravatar Guillaume Melquiond2014-10-27
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-04 14:45:10 +0000