aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc/refman
Commit message (Collapse)AuthorAge
* Addressing report #3279 (inconsistency of behavior of the -> and <-Gravatar Hugo Herbelin2014-10-24
| | | | | | | | | | | | | | | 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.
* Fix typo in documentation of the [repeat] tactical.Gravatar Arnaud Spiwack2014-10-24
| | | Closes #3761.
* Move 'Arguments: clear implicits' to 2.7.4 (Close 2891)Gravatar Enrico Tassi2014-10-22
|
* More fallout from elisp renameGravatar Anders Kaseorg2014-10-16
| | | | | | | | | | 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>
* Fixing #3606 continued (doc of Scheme Boolean Equality Scheme).Gravatar Hugo Herbelin2014-10-03
|
* Removing deactivated command Show Tree.Gravatar Hugo Herbelin2014-10-03
|
* typoGravatar Enrico Tassi2014-09-29
|
* Documenting option -type-in-type.Gravatar Hugo Herbelin2014-09-29
|
* seems to fix a looping coq-tex (when compiled with camlp4)Gravatar Pierre Boutillier2014-09-18
|
* Fixing bug #3605.Gravatar Pierre-Marie Pédrot2014-09-11
|
* Removing remaining documentation of the XML plugin.Gravatar Pierre-Marie Pédrot2014-09-11
|
* Fixing inversion after having fixed intros_replacingGravatar Hugo Herbelin2014-09-10
| | | | | | | 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.
* Removing "eqn:" for "induction" in reference manual.Gravatar Hugo Herbelin2014-09-10
|
* Documenting the new Undo semanticsGravatar Enrico Tassi2014-09-09
|
* Removing the documentation of the XML plugin.Gravatar Pierre-Marie Pédrot2014-09-08
|
* Doc: [revgoals].Gravatar Arnaud Spiwack2014-09-08
|
* Little fix in documentation of inversion.Gravatar Hugo Herbelin2014-09-07
|
* Documenting the [Variant] type definition and the [Nonrecursive Elimination ↵Gravatar Arnaud Spiwack2014-09-04
| | | | Schemes] option.
* sed -i.toto -e 's/Objective Caml/\{\ocaml\}/g' doc/refman/RefMan-*.texGravatar Pierre Boutillier2014-09-03
|
* Improve RefMan section about Coq_makefileGravatar Pierre Boutillier2014-09-03
|
* Update RefMan with respect to new loadpath managementGravatar Pierre Boutillier2014-09-03
|
* Cbn in refmanGravatar Pierre Boutillier2014-09-03
|
* coqworkmgrGravatar Enrico Tassi2014-09-02
|
* "allows to", like "allowing to", is improperGravatar Jason Gross2014-08-25
| | | | | | | | | | | 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).
* Grammar: "allowing to" is not proper EnglishGravatar Jason Gross2014-08-25
| | | | | | | | | | | 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.
* Adding a new intro-pattern for "apply in" on the fly. Using syntaxGravatar Hugo Herbelin2014-08-18
| | | | "pat/term" for "apply term on current_hyp as pat".
* Slight simplification of naming of tactics in equality.ml (hopefully).Gravatar Hugo Herbelin2014-08-18
| | | | Isolating a core tactic in replace, shareable to cutrewrite.
* Removing documentation related to the deprecated State machinery.Gravatar Pierre-Marie Pédrot2014-08-16
|
* Uncountably many bullets (+,-,*,++,--,**,+++,...).Gravatar Hugo Herbelin2014-08-05
|
* Experimentally adding an option for automatically erasing anGravatar Hugo Herbelin2014-08-05
| | | | | | | | | | 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).
* Adding a syntax "enough" for the variant of "assert" with the order ofGravatar Hugo Herbelin2014-08-05
| | | | subgoals and the role of the "by tac" clause swapped.
* Making references to Proof General and CoqIDE uniform in Reference Manual.Gravatar Hugo Herbelin2014-08-05
|
* Chapter 4 of reference manual: Fixing asymmetric patterns error +Gravatar Hugo Herbelin2014-08-05
| | | | no spacing in English before ":".
* Documentation: a simple example for [numgoals].Gravatar Arnaud Spiwack2014-08-05
| | | | Now that [idtac] can print a single message for several goals, printing the number of goals is readable.
* Documentation of [uconstr]: typesetting.Gravatar Arnaud Spiwack2014-08-05
|
* Documentation: refine accept uconstr arguments.Gravatar Arnaud Spiwack2014-08-05
|
* Doc: uconstr now has a tactic notation entry.Gravatar Arnaud Spiwack2014-08-05
|
* Chapter 4: Fixing ambiguity about whether the return predicate refersGravatar Hugo Herbelin2014-08-03
| | | | | explicitly or implicitly to the variables in the as and in clauses + formatting.
* Document [> … ].Gravatar Arnaud Spiwack2014-08-01
|
* Fix English spelling -> American spelling in doc.Gravatar Arnaud Spiwack2014-08-01
|
* Document [numgoals] and [guard].Gravatar Arnaud Spiwack2014-08-01
|
* Typos.Gravatar Hugo Herbelin2014-07-31
|
* Document untyped terms in tactics.Gravatar Arnaud Spiwack2014-07-29
|
* Document swap tactic.Gravatar Arnaud Spiwack2014-07-25
|
* Document cycle tactic.Gravatar Arnaud Spiwack2014-07-25
|
* Update the documentation of Ltac's ";" and ";[…]" to reflect the new ↵Gravatar Arnaud Spiwack2014-07-25
| | | | multi-goal semantics of tactics.
* Warns about inconsistency of generated name in evars and goals.Gravatar Arnaud Spiwack2014-07-25
| | | | See bug #1041
* More documentation of universes.Gravatar Matthieu Sozeau2014-07-25
|
* Start documenting universe polymorphism.Gravatar Matthieu Sozeau2014-07-24
|
* Derive plugin: document new syntax.Gravatar Arnaud Spiwack2014-07-23
|
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-08 23:36:58 +0000