aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc/refman/RefMan-tac.tex
Commit message (Collapse)AuthorAge
* use OCaml temp_file, instead of our own versionGravatar Paul Steckler2017-08-18
|
* Add native compute profiling, BZ#5170Gravatar Paul Steckler2017-08-17
|
* mention that tactic is the identity or gives errorGravatar Paul Steckler2017-08-16
|
* change section caption, improve some wordingGravatar Paul Steckler2017-08-16
|
* Fix documentation of Hint Mode (bug #4911).Gravatar Guillaume Melquiond2017-07-28
|
* Sync the manual with the deprecation warnings.Gravatar Théo Zimmermann2017-07-11
|
* Merge PR #837: Add inversion_sigma to CHANGES and to docGravatar Maxime Dénès2017-07-05
|\
* \ Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2017-07-04
|\ \
| | * Add doc for inversion_sigma to RefMan-tacGravatar Jason Gross2017-06-30
| |/ |/|
* | Merge PR#777: Improving documentation of tactic "move" (report #4561)Gravatar Maxime Dénès2017-06-19
|\ \
* | | Prelude : no more autoload of plugins extraction and recdefGravatar Pierre Letouzey2017-06-14
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The user now has to manually load them, respectively via: Require Extraction Require Import FunInd The "Import" in the case of FunInd is to ensure that the tactics functional induction and functional inversion are indeed in scope. Note that the Recdef.v file is still there as well (it contains complements used when doing Function with measures), and it also triggers a load of FunInd.v. This change is correctly documented in the refman, and the test-suite has been adapted.
| * | Improving documentation of tactic "move" (report #4561).Gravatar Hugo Herbelin2017-06-13
|/ /
| * Document instantiate (ident := term) and make it the preferred variant.Gravatar Théo Zimmermann2017-06-13
| |
* | Merge PR#449: make specialize smarter (bug 5370).Gravatar Maxime Dénès2017-06-01
|\ \
| * | Documenting the new behaviour of specialize.Gravatar Pierre Courtieu2017-05-31
| | |
* | | Documentation for eassert, eenough, epose proof, eset, eremember, epose.Gravatar Hugo Herbelin2017-05-30
|/ / | | | | | | Includes fixes and suggestions from Théo.
* | Documenting relaxing of constraints on injection.Gravatar Hugo Herbelin2017-05-17
| | | | | | | | | | We seized this opportunity to do a little refreshing of the section describing injection.
* | Improve documentation of assert / pose proof / specialize.Gravatar Théo Zimmermann2017-05-04
| | | | | | | | | | | | | | | | | | This commits documents the as clause of specialize and that the as clause of pose proof is optional. It also mentions a feature of assert ( := ) that was available since 8.5 and was mentionned by @herbelin in: https://github.com/coq/coq/pull/248#issuecomment-297970503
* | Fixing #5420 as well as many related bugs due to miscounting let-ins.Gravatar Hugo Herbelin2017-04-09
|/ | | | | | | | - Supporting let-ins in tactic "fix", and hence in interactive Fixpoint and mutual theorems. - Documenting more precisely the meaning of n in tactic "fix id n". - Fixing computation of recursive index at interpretation time in the presence of let-ins.
* Fix broken documentation in presence of \zeroone{... \tt ...}.Gravatar Guillaume Melquiond2016-12-06
| | | | | | | | | | | | | The way \zeroone was defined, the \tt modifier was leaked outside the brackets, thus messing with the following text. There are a bunch of occurrences of this issue in the manual, so rather than turning all the \tt into \texttt, the definition of \zeroone is made more robust. Unfortunately, there is one single occurrence of \zeroone that does not support the more robust version. (Note that this specific usage of \zeroone is morally a bug, since it goes against all the LaTeX conventions.) So the commit also keeps the old leaky version of \zeroone around as \zeroonelax so that it can be used there.
* Update documentation (bugs #5246 and #5251).Gravatar Guillaume Melquiond2016-12-06
|
* Merge remote-tracking branch 'github/pr/348' into v8.6Gravatar Maxime Dénès2016-11-08
|\ | | | | | | Was PR#348: Credits for 8.6
* \ Merge remote-tracking branch 'github/pr/339' into v8.6Gravatar Maxime Dénès2016-11-07
|\ \ | | | | | | | | | Was PR#339: Documenting type class options, typeclasses eauto
| * | Document two new variants of refineGravatar Matthieu Sozeau2016-11-07
| | | | | | | | | | | | | | | They allow to call refine without doing typeclass resolution, allowing to use refine in typeclass hints.
| | * Minor fix in documentationGravatar Matthieu Sozeau2016-11-05
| |/ |/|
* | Merge remote-tracking branch 'github/pr/336' into v8.6Gravatar Maxime Dénès2016-11-04
|\ \ | | | | | | | | | Was PR#336: Remove v62
| | * Lets Hints/Instances take an optional patternGravatar Matthieu Sozeau2016-11-03
| | | | | | | | | | | | | | | | | | | | | | | | | | | In addition to a priority, cleanup the interfaces for passing this information as well. The pattern, if given, takes priority over the inferred one. We only allow Existing Instances gr ... gr | pri. for now, without pattern, as before. Make the API compatible to 8.5 as well.
| | * Documenting changes in typeclassesGravatar Matthieu Sozeau2016-10-29
| |/ |/|
| * Remove v62 from the refman.Gravatar Théo Zimmermann2016-10-25
| |
* | Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2016-10-24
|\ \ | |/ |/|
| * Documenting Hint Resolve -> and <- variants.Gravatar Théo Zimmermann2016-10-19
| | | | | | | | These variants are from 8.3 but were never documented except in CHANGES.
| * Making the doc of auto hints more precise.Gravatar Théo Zimmermann2016-10-19
| | | | | | | | | | | | | | | | | | | | The doc of auto hints now mention again that sometimes a hint will be used with simple apply and sometimes it will be used with exact. It does not try to be fully precise in that we don't necessarily want to document the behaviors of auto that we might like to change. See also the discussion on commit 9227d6e.
| * Extending the doc with a general summary of auto variants.Gravatar Théo Zimmermann2016-10-18
| | | | | | | | | | This way of giving the summary avoids redundancy as much as possible. It is helpful for the auto-completion of Company-Coq of @cpitclaudel.
| * Document info_auto.Gravatar Théo Zimmermann2016-10-18
| | | | | | | | | | Now that this tactic has been fixed (commit 58d1381), it needed to get documented.
| * Improve the documentation of eauto.Gravatar Théo Zimmermann2016-10-18
| | | | | | | | | | | | | | | | Improve the description of what auto/eauto do. These two tactics rely on the simple version of apply/eapply. Since this simple version is available to the end user, it is better to mention it. See also the confusion that such description can create in the thread "Understanding auto" on Coq-Club.
* | fixing bug 4609: document an option governing the generation of equalitiesGravatar Yves Bertot2016-10-03
| | | | | | | | between proofs in tactic injection, with a side-effect on inversion.
* | Merge branch 'v8.5' into v8.6Gravatar Maxime Dénès2016-09-30
|\|
* | Merge remote-tracking branch 'github/pr/232' into v8.6Gravatar Maxime Dénès2016-09-28
|\ \ | | | | | | | | | Was PR#232: Fix the parsing of goal selectors.
| | * Fixing #4887 (confusion between using and with in documentation of firstorder).Gravatar Hugo Herbelin2016-09-27
| | |
* | | Extending "contradiction" so that it recognizes statements such as "~x=x" or ↵Gravatar Hugo Herbelin2016-09-15
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | ~True. Found 1 incompatibility in tested contribs and 3 times the same pattern of incompatibility in the standard library. In all cases, it is an improvement in the form of the script. New behavior deactivated when version is <= 8.5.
* | | Refolding: disable in 8.4 compat file, documentGravatar Matthieu Sozeau2016-09-12
| | |
* | | Documenting "Set Structural Injection".Gravatar Hugo Herbelin2016-08-21
| | |
* | | Add and document match, fix and cofix reduction flags.Gravatar Maxime Dénès2016-07-01
| | |
| * | Update the documentation for goal selectors.Gravatar Cyprien Mangin2016-06-30
|/ /
* | Updated CHANGES about subst. More on recursive equations in reference manual.Gravatar Hugo Herbelin2016-06-29
| |
* | Document new Hint Mode option.Gravatar Matthieu Sozeau2016-06-16
| |
* | Revise syntax of Hint CutGravatar Matthieu Sozeau2016-06-16
| | | | | | | | | | As noticed by C. Cohen it was confusingly different from standard notation.
* | Add documentation for goal selectors.Gravatar Cyprien Mangin2016-06-14
| |
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-05-04
|\|
| * In Regular Subst Tactic mode, ensure that the order of hypotheses isGravatar Hugo Herbelin2016-05-03
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | preserved, which is a source of incompatibilities w.r.t. released 8.5 but which looks to me to be the only possible canonical behavior. This is I believe a better behavior than the Regular Subst Tactic behavior in the released 8.5 and 8.5pl1. There, the order of hypotheses in which substitutions happened was respected, but their interleaving with other hypotheses was not respected. So, I consider this to be a fix to the "Regular Subst Tactic" mode. Also added a more detailed "specification" of the "Regular" behavior of "subst" in the reference manual.
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-05 06:32:04 +0000