aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc
Commit message (Collapse)AuthorAge
* Fix ltac's progress tactical: requires progress in each goal.Gravatar aspiwack2013-11-04
| | | | | | | | 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
* Doc: solve the bad interaction between Declare Implicit Tactic and refine.Gravatar aspiwack2013-11-02
| | | | | | 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
* Documentation for the backtracking features.Gravatar aspiwack2013-11-02
| | | | | | 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
* Adds a tactic give_up.Gravatar aspiwack2013-11-02
| | | | | | 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
* A tactic shelve_unifiable.Gravatar aspiwack2013-11-02
| | | | | | | | | | | | | 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
* Adds a shelve tactic.Gravatar aspiwack2013-11-02
| | | | | | 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
* Document "all:" and "Set Default Goal Selector".Gravatar aspiwack2013-11-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16984 85f007b7-540e-0410-9357-904b9bb8a0f7
* add "Print Ring" and "Print Field" vernacular commandsGravatar gareuselesinge2013-08-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16751 85f007b7-540e-0410-9357-904b9bb8a0f7
* Updating documentation of the ring/field tactics.Gravatar amahboub2013-08-23
| | | | | | | | 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
* Manual fixed w.r.t. STMGravatar gareuselesinge2013-08-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16675 85f007b7-540e-0410-9357-904b9bb8a0f7
* Documenting the Remove Hints command.Gravatar ppedrot2013-08-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16648 85f007b7-540e-0410-9357-904b9bb8a0f7
* Documenting the previous commit: Existing Instance with priority.Gravatar ppedrot2013-08-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16646 85f007b7-540e-0410-9357-904b9bb8a0f7
* Revising r16550 about providing intro patterns for applying injection:Gravatar herbelin2013-07-09
| | | | | | | | | | | | - 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
* Documenting a potential source of incompleteness in the ring tactic,Gravatar amahboub2013-06-17
| | | | | | | | 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
* Fixing #3056Gravatar ppedrot2013-06-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16566 85f007b7-540e-0410-9357-904b9bb8a0f7
* Document changes and add missing documentation for Program options.Gravatar msozeau2013-06-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16563 85f007b7-540e-0410-9357-904b9bb8a0f7
* Start documenting new [rewrite_strat] tactic that applies rewritingGravatar msozeau2013-06-04
| | | | | | | | | 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
* A constructive proof of Fan theorem where paths are represented by predicates.Gravatar herbelin2013-06-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16557 85f007b7-540e-0410-9357-904b9bb8a0f7
* Making the behavior of "injection ... as ..." more natural:Gravatar herbelin2013-06-02
| | | | | | | | | | | | | - 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
* Fixing a typo in the documentation of discriminate.Gravatar herbelin2013-06-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16551 85f007b7-540e-0410-9357-904b9bb8a0f7
* Documenting the "appcontext" by default.Gravatar ppedrot2013-05-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16539 85f007b7-540e-0410-9357-904b9bb8a0f7
* Documenting the previous commit.Gravatar ppedrot2013-05-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16513 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix typo in manualGravatar gareuselesinge2013-05-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16474 85f007b7-540e-0410-9357-904b9bb8a0f7
* Renaming SearchAbout into Search and Search into SearchHead.Gravatar herbelin2013-04-17
| | | | | | 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
* Small doc fix : module subtyping cannot force access of opaquesGravatar letouzey2013-04-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16385 85f007b7-540e-0410-9357-904b9bb8a0f7
* Revised infrastructure for lazy loading of opaque proofsGravatar letouzey2013-04-02
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Get rid of the LightenLibrary hack : no more last-minute collect of opaque terms and Obj.magic tricks. Instead, we make coqc accumulate the opaque terms as soon as constant_bodies are created outside sections. In these cases, the opaque terms are placed in a special table, and some (DirPath.t * int) are used as indexes in constant_body. In an interactive session, the local opaque terms stay directly stored in the constant_body. The structure of .vo file stays similar : magic number, regular library structure, digest of the first part, array of opaque terms. In addition, we now have a final checksum for checking the integrity of the whole .vo file. The other difference is that lazy_constr aren't changed into int indexes in .vo files, but are now coded as (substitution list * DirPath.t * int). In particular this approach allows to refer to opaque terms from another library. This (and accumulating substitutions in lazy_constr) seems to greatly help decreasing the size of opaque tables : -20% of vo size on the standard library :-). The compilation times are slightly better, but that can be statistic noise. The -force-load-proofs isn't active anymore : it behaves now just like -lazy-load-proofs. The -dont-load-proofs mode has slightly changed : opaque terms aren't seen as axioms anymore, but accessing their bodies will raise an error. Btw, API change : Declareops.body_of_constant now produces directly a constr option instead of a constr_substituted option git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16382 85f007b7-540e-0410-9357-904b9bb8a0f7
* Typo in refman (fix #2962)Gravatar letouzey2013-03-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16369 85f007b7-540e-0410-9357-904b9bb8a0f7
* Using hnf instead of "intro H" for forcing reduction to a product.Gravatar herbelin2013-03-21
| | | | | | | | Added full betaiota in hnf. This seems more natural, even if it changes the strict meaning of hnf. This is source of incompatibilities as "intro" might succeed more often. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16338 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing an old pecularity of "red": head betaiota redexes are nowGravatar herbelin2013-03-21
| | | | | | reduced in order to find some head constant to reduce. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16337 85f007b7-540e-0410-9357-904b9bb8a0f7
* Allowing (Co)Fixpoint to be defined local and Let-style.Gravatar ppedrot2013-03-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16266 85f007b7-540e-0410-9357-904b9bb8a0f7
* Documentation of the "Local Definition" command.Gravatar ppedrot2013-03-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16264 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added missing documentation of Set Printing Existential Instances.Gravatar herbelin2013-02-21
| | | | | | | Also started a preliminary documentation about evars (where to have it in the doc is somehow open). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16234 85f007b7-540e-0410-9357-904b9bb8a0f7
* Documenting the 'Printing Transparent/All Dependencies' command.Gravatar ppedrot2012-10-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15946 85f007b7-540e-0410-9357-904b9bb8a0f7
* RefMan-tac: fix a few glitches concerning the documentation of eqn:Gravatar letouzey2012-10-23
| | | | | | | These were introduced during Guillaume's backport to trunk of its improved tactic documentation git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15920 85f007b7-540e-0410-9357-904b9bb8a0f7
* Move reflexivity, symmetry, and transitivity, next to f_equal, in the ↵Gravatar gmelquio2012-09-16
| | | | | | documentation. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15812 85f007b7-540e-0410-9357-904b9bb8a0f7
* Some more fixes to tactic documentation.Gravatar gmelquio2012-09-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15811 85f007b7-540e-0410-9357-904b9bb8a0f7
* Beautify tactic documentation a bit more.Gravatar gmelquio2012-09-16
| | | | | | | | - Do not use \\ in place of empty lines. - Fix missing spaces after some \dots. - Do not use monospace slanted for clauses. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15810 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remove superfluous spaces and commas in tactic documentation.Gravatar gmelquio2012-09-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15809 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix index generation for the pdf document.Gravatar gmelquio2012-09-16
| | | | | | | In particular, push all the \tacindex commands outside of the section titles, as they break index generation when put inside. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15808 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix failure to compile doc/stdlib/Library.tex.Gravatar gmelquio2012-09-15
| | | | | | | | | | | | | | | | Coqdoc converts the utf8 symbol lambda (that appears in Utf8_core.v) to itself when outputting utf8. Since Library.tex uses utf8x as the input encoding, it gets translated to \textlambda. This command is defined by both the LGR font encoding and the tipa package, and only by them. So the build fails. There are several solutions: 1. \usepackage[mathletters]{ucs} 2. \usepackage[T1,LGR]{fontenc} 3. \usepackage{tipa} 4. modify coqdoc git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15807 85f007b7-540e-0410-9357-904b9bb8a0f7
* Port rewrites of tactic documentation from branch 8.4.Gravatar gmelquio2012-09-15
| | | | | | | | This encompasses commits r15183, r15190, r15243, r15262, r15276, r15277, r15278, r15337. The merge did not go without troubles, but hopefully none of the changes were lost in process. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15806 85f007b7-540e-0410-9357-904b9bb8a0f7
* Obsolete syntax in documentation of Solve Obligation commands.Gravatar ppedrot2012-09-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15778 85f007b7-540e-0410-9357-904b9bb8a0f7
* Add option Set/Unset Extraction Conservative Types.Gravatar aspiwack2012-08-24
| | | | | | | | | | | | | | | | | Extracted code need not preserve typing relations (e:t) from the source code. This may be a problem as the extracted code may not implement the intented interface. This option disables the optimisations which would prevent an extracted term's type to be its extracted source term's type. At this point the only such optimization is (I think) removing some dummy λ-abstractions in constant definitions. Extraction Implicit is still honored in this mode, and it's mostly necessary to produce reasonable types. So in the conservative type mode, which abstractions can be removed and which can'tt is entirely under the user's control. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15762 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remove a script unused since 2006 (cf commit r8626)Gravatar letouzey2012-08-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15755 85f007b7-540e-0410-9357-904b9bb8a0f7
* Extraction: document Separate Extraction and KeepSingletonGravatar letouzey2012-08-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15746 85f007b7-540e-0410-9357-904b9bb8a0f7
* Improving rendering of ldots in doc (partially done, there are tooGravatar herbelin2012-08-11
| | | | | | much of them). Improving doc of conversion clauses. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15733 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added support for option Local (at module level) in Tactic Notation.Gravatar herbelin2012-08-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15731 85f007b7-540e-0410-9357-904b9bb8a0f7
* Improving rendering of ...-separated lists and sequences in referenceGravatar herbelin2012-08-11
| | | | | | | manual (making style uniform: no {\tt \ldots}; using only one space when there is no delimiters in the sequence). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15729 85f007b7-540e-0410-9357-904b9bb8a0f7
* Updating version numbers.Gravatar herbelin2012-08-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15709 85f007b7-540e-0410-9357-904b9bb8a0f7
* Documenting eta-conversion.Gravatar herbelin2012-08-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15708 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-28 08:03:08 +0000