aboutsummaryrefslogtreecommitdiff
path: root/doc
AgeCommit message (Collapse)Author
2014-06-13Remove documentation for the unsupported options -byte and -opt.Guillaume Melquiond
2014-06-13Deprecate 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-31More 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-08Typo reference manualHugo Herbelin
2014-05-06- Fix index-list to show computational relations for rewriting files.Matthieu Sozeau
- Fix hasheq which didn't have a case for Proj making hashconsing exponentially slower. Conflicts: kernel/constr.ml kernel/univ.ml proofs/proof_global.ml
2014-04-28Prevent coq_tex from generating curly quotes. (Partial fix for bug #2964)Guillaume Melquiond
2014-04-05Completing text of the question on conservativity of CIC over CC (bug #2697).Hugo Herbelin
2014-04-04Fix for bug #3107.Guillaume Melquiond
2014-04-04fixing Function docJulien Forest
2014-04-02Fix Bug 3131 + Really drop mentions of info in refman.Pierre Boutillier
2014-03-20Documenting the Print Strategy command.Pierre-Marie Pédrot
2014-02-26refman: document vi2voEnrico Tassi
2014-02-24fixup complement FinPierre Boutillier
2014-02-02Removing the [Require "file"] syntax.Pierre-Marie Pédrot
2014-01-26-schedule-vi-checking ported to spawnEnrico Tassi
2014-01-13Fixing typo in reference manual from previous commitHugo Herbelin
2014-01-13Documenting 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-05refman: fist stab at Asynchronous ProofsEnrico Tassi
2014-01-01Reference the 'external' tactic.Guillaume Melquiond
2013-12-20micromega: removal of spurious Export; addition of Lia.v encapsulating lia ↵Frédéric Besson
and nia.
2013-12-11Documenting the tactic-in-term construction.Pierre-Marie Pédrot
2013-12-06Missing 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-04Documentation 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-03Silence some warning about references in documentation.Guillaume Melquiond
2013-11-29First stab at documenting Canonical StructuresEnrico Tassi
2013-11-04Fix 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-02Doc: 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
2013-11-02Documentation for the backtracking features.aspiwack
This required some reorganisation of the documentation of existing tacticals. I hope the result is consistent. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17029 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-02Adds a tactic give_up.aspiwack
Gives up on the focused goals. Shows an unsafe status. Unlike the admit tactic, the proof cannot be closed until the users goes back and solves these goals. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17018 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-02A tactic shelve_unifiable.aspiwack
Puts on the shelf every goals under focus on which other goals under focus depend. Useful when we want to solve these goals by unification (as in a first order proof search procedure, for instance). Also meant to be able to recover approximately the semantics of the old refine with the new implementation (use refine t; shelve_unifiable). TODO: bug dans l'example de shelve_unifiable git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17017 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-02Adds a shelve tactic.aspiwack
The shelve tactic puts all the focused goals out of sight. They can be later recalled by the Unshelve command. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17013 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-02Document "all:" and "Set Default Goal Selector".aspiwack
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16984 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-08-30add "Print Ring" and "Print Field" vernacular commandsgareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16751 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-08-23Updating documentation of the ring/field tactics.amahboub
Removes the requirements that are obsolete after commit r16730. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16731 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-08-08Manual fixed w.r.t. STMgareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16675 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-08-01Documenting the Remove Hints command.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16648 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-08-01Documenting the previous commit: Existing Instance with priority.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16646 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-07-09Revising r16550 about providing intro patterns for applying injection:herbelin
- Introduction of a specific notation for injection intropatterns: [= pats] - Use of this specific pattern also to apply discriminate on the fly Note: The automatic injection of dependent tuples over a same first component (introduced in r10180) still not integrated to the main parts of injection and its variant (indeed, it applies only for a root dependent tuple in sigT). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16621 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-06-17Documenting a potential source of incompleteness in the ring tactic,amahboub
when reification is customized with a user-defined set of coefficients. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16583 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-06-06Fixing #3056ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16566 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-06-06Document changes and add missing documentation for Program options.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16563 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-06-04Start documenting new [rewrite_strat] tactic that applies rewritingmsozeau
according to a given strategy. - Enhance the hints/lemmas strategy to support "using tac" comming from rewrite hints to solve side-conditions. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16558 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-06-02A constructive proof of Fan theorem where paths are represented by predicates.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16557 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-06-02Making the behavior of "injection ... as ..." more natural:herbelin
- hypotheses are introduced in the left-to-right order - intropatterns have to match the number of generated hypotheses, and, if less, new introduction names are automatically generated - clearing the hypothesis on which injection is applied, if any. However, this is a source of incompatibilities (for a variant of injection that is hopefully not used a lot). Compatibility can be restored by "Unset Injection L2R Pattern Order". git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16556 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-06-02Fixing a typo in the documentation of discriminate.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16551 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-05-29Documenting the "appcontext" by default.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16539 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-05-12Documenting the previous commit.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16513 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-05-06Fix typo in manualgareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16474 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-04-17Renaming SearchAbout into Search and Search into SearchHead.herbelin
I hope I did not forget any place to change. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16423 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-04-04Small doc fix : module subtyping cannot force access of opaquesletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16385 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-10 05:01:34 +0000