aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc
Commit message (Collapse)AuthorAge
* 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.
* Document options of typeclasses (eauto)Gravatar Matthieu Sozeau2016-11-03
| | | | With update after J. Gross comments
* Documenting changes in typeclassesGravatar Matthieu Sozeau2016-10-29
|
* 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 remote-tracking branch 'github/pr/280' into v8.6Gravatar Maxime Dénès2016-09-30
|\ \ | | | | | | | | | | | | Was PR#280: Document that [Reset Ltac Profile] is not synchronized with the document state
* \ \ 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
| | | |
* | | | Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2016-09-23
|\ \ \ \ | | |/ / | |/| |
| * | | Replace { command ; } with ( command )Gravatar Erik Martin-Dorel2016-09-19
| | | | | | | | | | | | | | | | | | | | as suggested by Hugo. Also, escape the spaces after the dots to obtain a better PdfLaTeX output.
| * | | Fix typos in RefMan-uti.tex.Gravatar Erik Martin-Dorel2016-09-19
| | | | | | | | | | | | | | | | | | | | | | | | - Ensure "coq_makefile --help" is properly typeset with HeVeA/PdfLaTeX - Replace 's with "s so they are typeset as true ASCII characters - Add missing ; before closing brace.
| | | * Doc: [Reset Ltac Profile] is not synchronizedGravatar Jason Gross2016-09-16
| |_|/ |/| |
* | | 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
| | |
* | | Fix a typo in the reference manualGravatar Jason Gross2016-09-07
| | |
* | | plugin micromega : nra also handles non-linear rational arithmetic over Q ↵Gravatar Frédéric Besson2016-08-30
| | | | | | | | | | | | | | | | | | | | | (Fixed #4985) Lqa.v defines the tactics lra and nra working over Q. Lra.v defines the tactics lra and nra working over R.
* | | update Proof General URLGravatar Paul Steckler2016-08-23
| | |
* | | Documenting "Set Structural Injection".Gravatar Hugo Herbelin2016-08-21
| | |
* | | In docs, fix command to reset Ltac profilingGravatar Paul Steckler2016-08-17
| | |
* | | Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2016-08-16
|\| |
| * | Fix documentation typo (bug #4994).Gravatar Guillaume Melquiond2016-08-04
| | |
* | | More examples of recursive notations, with emphasis in reference manual.Gravatar Hugo Herbelin2016-07-17
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Further work would include: - Identify binders up to alpha-conversion (see #4932 with a list of binders of length at least 2, or #4592 on printing notations such as ex2). A cool example that one could also consider supporting: - Notation "[[ a , .. , b | .. | a , .. , b ]]" := (cons (cons a .. (cons b nil) ..) .. (cons a .. (cons b nil) ..) ..).
* | | Fix #4793: Coq 8.6 should accept -compat 8.6Gravatar Maxime Dénès2016-07-06
| | | | | | | | | | | | We also add a Coq86.v compat file.
* | | 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
| |
* | Fixes in documentation.Gravatar Matthieu Sozeau2016-06-29
| |
* | Program: cleanup in cases, add optionsGravatar Matthieu Sozeau2016-06-29
| | | | | | | | | | | | | | Unset Program Generalized Coercion to avoid coercion of general applications. Unset Program Cases to deactivate generation equalities and disequalities of cases.
* | Merge remote-tracking branch 'github/pr/207' into trunkGravatar Maxime Dénès2016-06-28
|\ \ | | | | | | | | | Was PR#207: Add -no-print-dependent-evars
* | | Documenting the "only printing" notation flag.Gravatar Pierre-Marie Pédrot2016-06-28
| | |
* | | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-06-27
|\ \ \ | | |/ | |/|
* | | Adding ability to put any pattern in binders, prefixed by a quote.Gravatar Daniel de Rauglaudre2016-06-27
| | | | | | | | | | | | Cf CHANGES for details.
| * | Reference Manual / Extraction: the original example command no longer works ↵Gravatar Matej Kosik2016-06-20
| | | | | | | | | | | | with recent Coq
| | * Add [Unset Printing Dependent Evars Line]Gravatar Jason Gross2016-06-19
| |/ |/| | | | | | | This allows a work-around for bug #4819, https://coq.inria.fr/bugs/show_bug.cgi?id=4819.
* | par: like all: but in parallelGravatar Enrico Tassi2016-06-17
| | | | | | | | | | | | | | | | | | | | | | | | | | This commit documents par:, fixes its semantics so that is behaves like all:, supports (toplevel) abstract and optimizes toplevel solve. `par: solve [tac]` is equivalent to `Ltac tac1 := solve[tac]...par: tac1` but is optimized for failures: if one goal fails all are aborted immediately. `par: abstract tac` runs abstract on the generated proof terms. Nested abstract calls are not supported.
* | 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.
* | Merge 'pr/191' into trunkGravatar Enrico Tassi2016-06-16
|\ \
* | | typographyGravatar Matej Kosik2016-06-15
| | |
| * | Add documentation for goal selectors.Gravatar Cyprien Mangin2016-06-14
| | |
* | | -async-proofs-delegation-threshold default value set to 0.03Gravatar Enrico Tassi2016-06-14
| | | | | | | | | | | | Documentation also updated.
* | | Merge remote-tracking branch 'origin/pr/173' into trunkGravatar Enrico Tassi2016-06-14
|\ \ \ | |/ / |/| | | | | This is the "error resiliency" mode for STM
* | | Merge branch "LtacProf for trunk" (PR #165).Gravatar Pierre-Marie Pédrot2016-06-14
|\ \ \
* | | | Univs: more robust Universe/Constraint decls #4816Gravatar Matthieu Sozeau2016-06-13
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This fixes the declarations of constraints, universes and assumptions: - global constraints can refer to global universes only, - polymorphic universes, constraints and assumptions can only be declared inside sections, when all the section's variables/universes are polymorphic as well. - monomorphic assumptions may only be declared in section contexts which are not parameterized by polymorphic universes/assumptions. Add fix for part 1 of bug #4816
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-06 04:54:20 +0000