aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc/refman
Commit message (Collapse)AuthorAge
* Tentatively updating credits while remaining brief.Gravatar Hugo Herbelin2015-01-15
|
* Reference manual: I had previously omitted the syntax entry for [> t1|…|tn].Gravatar Arnaud Spiwack2015-01-14
|
* Reference manual: document tryif/then/else.Gravatar Arnaud Spiwack2015-01-14
|
* Reference manual: document multimatch.Gravatar Arnaud Spiwack2015-01-14
|
* Reference manual: try and improve documentation for Ltac's match.Gravatar Arnaud Spiwack2015-01-14
| | | | In particular document the "once" behaviour.
* Reference manual: try and improve the documentation of lazymatch.Gravatar Arnaud Spiwack2015-01-14
| | | | In particular try to avoid the use of the word "backtracking" which refers to too many things.
* Reference manual: document gfail.Gravatar Arnaud Spiwack2015-01-14
|
* More documentation of the Local Definitions and Axioms.Gravatar Pierre-Marie Pédrot2015-01-13
|
* some credits for STMGravatar Enrico Tassi2015-01-11
|
* Start credits for 8.5.Gravatar Matthieu Sozeau2015-01-08
|
* Fixed and extend bullet related info/error messages. + doc.Gravatar Pierre Courtieu2015-01-08
| | | | | Had to put some hook in the handler of Proofview.NoSuchgoals. Documentation updated. CHANGE updated.
* Fix some documentation typos.Gravatar Guillaume Melquiond2015-01-08
|
* Document native_compute.Gravatar Maxime Dénès2015-01-08
|
* rename: vi -> vioGravatar Enrico Tassi2015-01-06
|
* Fix some documentation typos.Gravatar Guillaume Melquiond2015-01-06
|
* Added more informative messages about bullets.Gravatar Pierre Courtieu2015-01-05
| | | | Updated doc, but not tests-suite yet.
* Updating documentation about bullets.Gravatar Pierre Courtieu2015-01-05
| | | | Error messages were outdated.
* Document the new behavior of lazymatch.Gravatar Guillaume Melquiond2014-12-30
|
* Document 6d5b56d971 (forbid Require inside modules).Gravatar Maxime Dénès2014-12-25
|
* Better doc and a few fixes for Proof using.Gravatar Enrico Tassi2014-12-19
|
* Proof using: New vernacular to name sets of section variablesGravatar Enrico Tassi2014-12-18
|
* Searchxxx now search also the hypothesis and support goal selector.Gravatar Pierre Courtieu2014-12-12
| | | | Documentation also updated.
* refman: switch all source files to utf8Gravatar Pierre Letouzey2014-12-09
| | | | | | Putting utf8 everywhere helps the maintainance of the online refman. And anyway, this is the way to go. We should also chase and migrate the few remaining iso-latin-1 files elsewhere in the sources.
* refman: fix broken urlsGravatar Pierre Letouzey2014-12-09
|
* refman/Omega.tex: do not advertize Pierre Cregut's email for bug reportsGravatar Pierre Letouzey2014-12-09
|
* refman/coqdoc.tex: fix two erroneous \urlGravatar Pierre Letouzey2014-12-09
|
* refman: for xhtml validity, add 'alt' attributes to imgGravatar Pierre Letouzey2014-12-09
|
* refman: avoid label names with whitespace (unsupported in html)Gravatar Pierre Letouzey2014-12-09
|
* Documenting the Set Refine Instance Mode.Gravatar Pierre-Marie Pédrot2014-11-30
|
* typosGravatar Enrico Tassi2014-11-27
|
* Documenting the -color option.Gravatar Pierre-Marie Pédrot2014-11-17
|
* Documenting use of colors in Coq.Gravatar Pierre-Marie Pédrot2014-11-17
|
* Enforcing a stronger difference between the two syntaxes "simplGravatar Hugo Herbelin2014-11-16
| | | | | | | | | | | | | | | | | | | | | | | | | | | reference" and "simpl pattern" in the code (maybe we should have merged them instead, but I finally decided to enforce their difference, even if some compatibility is to be preversed - the idea is that at some time "simpl reference" would only call a weak-head simpl (or eventually cbn), leading e.g. to reduce 2+n into S(1+n) rather than S(S(n)) which could be useful for better using induction hypotheses. In the process we also implement the following: - 'simpl "+"' is accepted to reduce all applicative subterms whose head symbol is written "+" (in the toplevel scope); idem for vm_compute and native_compute - 'simpl reference' works even if reference has maximally inserted implicit arguments (this solves the "simpl fst" incompatibility) - compatibility of ltac expressions referring to vm_compute and native_compute with functor application should now work (i.e. vm_compute and native_compute are now taken into account in tacsubst.ml) - for compatibility, "simpl eq" (assuming no maximal implicit args in eq) or "simpl @eq" to mean "simpl (eq _ _)" are still allowed. By the way, is "mul" on nat defined optimally? "3*n" simplifies to "n+(n+(n+0))". Are there some advantages of this compared to have it simplified to "n+n+n" (i.e. to "(n+n)+n").
* Document (some) Proof using syntax + the new Optimize commandsGravatar Enrico Tassi2014-11-12
|
* Fixing doc of Functional Induction.Gravatar Hugo Herbelin2014-11-07
|
* Documenting the change of semantics of the replace tactic.Gravatar Pierre-Marie Pédrot2014-11-04
|
* Document [Info] command.Gravatar Arnaud Spiwack2014-11-01
|
* 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
|
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-09 06:15:04 +0000