| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2014-08-05 | Experimentally adding an option for automatically erasing an | Hugo Herbelin | |
| hypothesis when using it in apply or rewrite (prefix ">", undocumented), and a modifier to explicitly keep it in induction or destruct (prefix "!", reminiscent of non-linerarity). Also added undocumented option "Set Default Clearing Used Hypotheses" which makes apply and rewrite default to erasing the hypothesis they use (if ever their argument is indeed an hypothesis of the context). | |||
| 2014-08-05 | Adding a syntax "enough" for the variant of "assert" with the order of | Hugo Herbelin | |
| subgoals and the role of the "by tac" clause swapped. | |||
| 2014-08-05 | Making references to Proof General and CoqIDE uniform in Reference Manual. | Hugo Herbelin | |
| 2014-08-05 | Chapter 4 of reference manual: Fixing asymmetric patterns error + | Hugo Herbelin | |
| no spacing in English before ":". | |||
| 2014-08-05 | Documentation: a simple example for [numgoals]. | Arnaud Spiwack | |
| Now that [idtac] can print a single message for several goals, printing the number of goals is readable. | |||
| 2014-08-05 | Documentation of [uconstr]: typesetting. | Arnaud Spiwack | |
| 2014-08-05 | Documentation: refine accept uconstr arguments. | Arnaud Spiwack | |
| 2014-08-05 | Doc: uconstr now has a tactic notation entry. | Arnaud Spiwack | |
| 2014-08-03 | Chapter 4: Fixing ambiguity about whether the return predicate refers | Hugo Herbelin | |
| explicitly or implicitly to the variables in the as and in clauses + formatting. | |||
| 2014-08-01 | Document [> … ]. | Arnaud Spiwack | |
| 2014-08-01 | Fix English spelling -> American spelling in doc. | Arnaud Spiwack | |
| 2014-08-01 | Document [numgoals] and [guard]. | Arnaud Spiwack | |
| 2014-07-31 | Typos. | Hugo Herbelin | |
| 2014-07-29 | Document untyped terms in tactics. | Arnaud Spiwack | |
| 2014-07-25 | Document swap tactic. | Arnaud Spiwack | |
| 2014-07-25 | Document cycle tactic. | Arnaud Spiwack | |
| 2014-07-25 | Update the documentation of Ltac's ";" and ";[…]" to reflect the new ↵ | Arnaud Spiwack | |
| multi-goal semantics of tactics. | |||
| 2014-07-25 | Warns about inconsistency of generated name in evars and goals. | Arnaud Spiwack | |
| See bug #1041 | |||
| 2014-07-25 | More documentation of universes. | Matthieu Sozeau | |
| 2014-07-24 | Start documenting universe polymorphism. | Matthieu Sozeau | |
| 2014-07-23 | Derive plugin: document new syntax. | Arnaud Spiwack | |
| 2014-07-21 | Documenting the changes of Locate semantics. | Pierre-Marie Pédrot | |
| 2014-07-13 | Adding a "time" tactical for benchmarking purposes. In case the tactic | Hugo Herbelin | |
| backtracks, print time spent in each of successive calls. | |||
| 2014-07-01 | Continuing ff9f94634 on making code and doc agree on "Set Equality Schemes" | Hugo Herbelin | |
| 2014-06-21 | Fixing grammar in doc of Opaque as proposed by Jason (#3389). | Hugo Herbelin | |
| 2014-06-13 | Deprecate useless option -quality. | Guillaume Melquiond | |
| 2014-06-13 | Remove documentation for the unsupported options -byte and -opt. | Guillaume Melquiond | |
| 2014-06-13 | Deprecate options -dont, -lazy, -force-load-proofs. | Guillaume Melquiond | |
| These options no longer have any impact on the way proofs are loaded. In other words, loading is always lazy, whatever the options. Keeping them just so that coqc dies when the user prints some opaque symbol does not seem worth it. | |||
| 2014-05-31 | More on injection over a projectable "existT". - Fixing syntax "injection ↵ | Hugo Herbelin | |
| ... as ..." which was not working. - Now applying the simplification on any "existT" generated by "injection" (possible source of incompatibilities). | |||
| 2014-05-08 | Typo reference manual | Hugo Herbelin | |
| 2014-04-28 | Prevent coq_tex from generating curly quotes. (Partial fix for bug #2964) | Guillaume Melquiond | |
| 2014-04-04 | Fix for bug #3107. | Guillaume Melquiond | |
| 2014-04-04 | fixing Function doc | Julien Forest | |
| 2014-04-02 | Fix Bug 3131 + Really drop mentions of info in refman. | Pierre Boutillier | |
| 2014-03-20 | Documenting the Print Strategy command. | Pierre-Marie Pédrot | |
| 2014-02-26 | refman: document vi2vo | Enrico Tassi | |
| 2014-02-02 | Removing the [Require "file"] syntax. | Pierre-Marie Pédrot | |
| 2014-01-26 | -schedule-vi-checking ported to spawn | Enrico Tassi | |
| 2014-01-13 | Fixing typo in reference manual from previous commit | Hugo Herbelin | |
| 2014-01-13 | Documenting old but useful command "Print Tables". | Hugo Herbelin | |
| Made a synonymous of it ("Print Options"). Also reorganized a bit the section about flags and options in reference manual. | |||
| 2014-01-05 | refman: fist stab at Asynchronous Proofs | Enrico Tassi | |
| 2014-01-01 | Reference the 'external' tactic. | Guillaume Melquiond | |
| 2013-12-20 | micromega: removal of spurious Export; addition of Lia.v encapsulating lia ↵ | Frédéric Besson | |
| and nia. | |||
| 2013-12-11 | Documenting the tactic-in-term construction. | Pierre-Marie Pédrot | |
| 2013-12-06 | Missing file in commit 1fb883. | Arnaud Spiwack | |
| It would seem that I forgot to include the actual documentation in 1fb883. As a result, the reference manual didn't compile due to missing dependencies. | |||
| 2013-12-04 | Documentation of the Derive plugin. | Arnaud Spiwack | |
| I put it in a new chapter of the Addendum of the manual. Which is meant to be dedicated to plugins with short documentation. | |||
| 2013-12-03 | Silence some warning about references in documentation. | Guillaume Melquiond | |
| 2013-11-29 | First stab at documenting Canonical Structures | Enrico Tassi | |
| 2013-11-04 | Fix ltac's progress tactical: requires progress in each goal. | aspiwack | |
| Proofview.tclPROGRESS considers that a tactic that changes the list of goal progresses, under this semantics, "progress auto" succeeds if its applied to two goals and solves the first one but not the second one. This would break backwards compatibility. Spotted in Fermat4. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17058 85f007b7-540e-0410-9357-904b9bb8a0f7 | |||
| 2013-11-02 | Doc: solve the bad interaction between Declare Implicit Tactic and refine. | aspiwack | |
| An implicit tactic was declared and made refine fail (trying to solve the open goals of the refined term resulted in an error). There was no way to remove the implicit tactic (it isn't managed by an option so isn't removed by Reset Initial). I added the option under the name Clear Implicit Tactic. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17032 85f007b7-540e-0410-9357-904b9bb8a0f7 | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |