| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2014-11-12 | Document (some) Proof using syntax + the new Optimize commands | Enrico Tassi | |
| 2014-11-07 | Fixing doc of Functional Induction. | Hugo Herbelin | |
| 2014-11-04 | Documenting the change of semantics of the replace tactic. | Pierre-Marie Pédrot | |
| 2014-11-01 | Document [Info] command. | Arnaud Spiwack | |
| 2014-10-24 | Addressing report #3279 (inconsistency of behavior of the -> and <- | Hugo Herbelin | |
| introduction patterns). Whether we call -> and <- from assert as or apply in as, or as a component of a larger introduction pattern, the new documented semantics is: - behave as subst if an equation rewriting a variable (rewrite in conclusion and hyps and erase variable and hyp). - rewrite in concl if an equation not rewrite a variable or a quantified equality, then erase the hypothesis. This is potential source of incompatibilities. | |||
| 2014-10-24 | Fix typo in documentation of the [repeat] tactical. | Arnaud Spiwack | |
| Closes #3761. | |||
| 2014-10-22 | Move 'Arguments: clear implicits' to 2.7.4 (Close 2891) | Enrico Tassi | |
| 2014-10-16 | More fallout from elisp rename | Anders Kaseorg | |
| Commit 3e972b3ff8e532be233f70567c87512324c99b4e renamed coq.el, coq-db.el, coq-syntax.el to gallina.el, gallina-db.el, gallina-syntax.el without fixing up any of the references. Commit 30b58d43e48569afb50a35d3915ec7d453a61f5d only fixed up some of them. Here are some more (hopefully all of them). Signed-off-by: Anders Kaseorg <andersk@mit.edu> | |||
| 2014-10-03 | Fixing #3606 continued (doc of Scheme Boolean Equality Scheme). | Hugo Herbelin | |
| 2014-10-03 | Removing deactivated command Show Tree. | Hugo Herbelin | |
| 2014-09-29 | typo | Enrico Tassi | |
| 2014-09-29 | Documenting option -type-in-type. | Hugo Herbelin | |
| 2014-09-18 | seems to fix a looping coq-tex (when compiled with camlp4) | Pierre Boutillier | |
| 2014-09-11 | Fixing bug #3605. | Pierre-Marie Pédrot | |
| 2014-09-11 | Removing remaining documentation of the XML plugin. | Pierre-Marie Pédrot | |
| 2014-09-10 | Fixing inversion after having fixed intros_replacing | Hugo Herbelin | |
| in69665dd2480d364162933972de7ffa955eccab4d. There are still situations when "as" is not given where equations coming from injection are not yet removed, making invalid the computation of dependencies, what prevents an hypothesis to be cleared and replaced. | |||
| 2014-09-10 | Removing "eqn:" for "induction" in reference manual. | Hugo Herbelin | |
| 2014-09-09 | Documenting the new Undo semantics | Enrico Tassi | |
| 2014-09-08 | Removing the documentation of the XML plugin. | Pierre-Marie Pédrot | |
| 2014-09-08 | Doc: [revgoals]. | Arnaud Spiwack | |
| 2014-09-07 | Little fix in documentation of inversion. | Hugo Herbelin | |
| 2014-09-04 | Documenting the [Variant] type definition and the [Nonrecursive Elimination ↵ | Arnaud Spiwack | |
| Schemes] option. | |||
| 2014-09-03 | sed -i.toto -e 's/Objective Caml/\{\ocaml\}/g' doc/refman/RefMan-*.tex | Pierre Boutillier | |
| 2014-09-03 | Improve RefMan section about Coq_makefile | Pierre Boutillier | |
| 2014-09-03 | Update RefMan with respect to new loadpath management | Pierre Boutillier | |
| 2014-09-03 | Cbn in refman | Pierre Boutillier | |
| 2014-09-02 | coqworkmgr | Enrico Tassi | |
| 2014-08-25 | "allows to", like "allowing to", is improper | Jason Gross | |
| It's possible that I should have removed more "allows", as many instances of "foo allows to bar" could have been replaced by "foo bars" (e.g., "[Qed] allows to check and save a complete proof term" could be "[Qed] checks and saves a complete proof term"), but not always (e.g., "the optional argument allows to ignore universe polymorphism" should not be "the optional argument ignores universe polymorphism" but "the optional argument allows the caller to instruct Coq to ignore universe polymorphism" or something similar). | |||
| 2014-08-25 | Grammar: "allowing to" is not proper English | Jason Gross | |
| I'm not quite sure why, but I'm pretty sure it's not. Rather, in "allowing for foo" and "allowing to foo", "foo" modifies the sense in which someting is allowed, rather than it being "foo" that's allowed. "Allowing fooing" generally works, though it can sound a bit awkward. "Allowing one to foo" (or "Allowing {him,her,it,Coq} to foo") is always acceptable, in-as-much as it's ok to use "one". I haven't touched the older instances of it in the CHANGES file. | |||
| 2014-08-18 | Adding a new intro-pattern for "apply in" on the fly. Using syntax | Hugo Herbelin | |
| "pat/term" for "apply term on current_hyp as pat". | |||
| 2014-08-18 | Slight simplification of naming of tactics in equality.ml (hopefully). | Hugo Herbelin | |
| Isolating a core tactic in replace, shareable to cutrewrite. | |||
| 2014-08-16 | Removing documentation related to the deprecated State machinery. | Pierre-Marie Pédrot | |
| 2014-08-05 | Uncountably many bullets (+,-,*,++,--,**,+++,...). | Hugo Herbelin | |
| 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. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |