| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 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. | |||
| 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 | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |