aboutsummaryrefslogtreecommitdiff
path: root/doc/sphinx/proof-engine
AgeCommit message (Collapse)Author
2019-08-16Add documentation for typing flags.SimonBoulier
2019-08-08Merge PR #10324: Fix #10088: Ltac2 & operator conflicts with notations ↵Maxime Dénès
involving & Reviewed-by: Zimmi48 Ack-by: ejgallego Reviewed-by: gares Ack-by: ggonthier Ack-by: herbelin Reviewed-by: maximedenes Ack-by: vbgl
2019-08-08[ssr] Refactor under's Setoid generalization to ease stdlib2 portingErik Martin-Dorel
Changes: * Add ssrclasses.v that redefines [Reflexive] and [iff_Reflexive]; * Add ssrsetoid.v that links [ssrclasses.Reflexive] and [RelationClasses.Reflexive]; * Add [Require Coq.ssr.ssrsetoid] in Setoid.v; * Update ssrfwd.ml accordingly, using a helper file ssrclasses.ml that ports some non-exported material from rewrite.ml; * Some upside in passing: ssrfwd.ml no more depends on Ltac_plugin; * Update doc and tests as well. Summary: * We can now use the under tactic in two flavors: - with the [eq] or [iff] relations: [Require Import ssreflect.] - or a [RewriteRelation]: [Require Import ssreflect. Require Setoid.] (while [ssreflect] does not require [RelationClasses] nor [Setoid], and conversely [Setoid] does not require [ssreflect]). * The file ssrsetoid.v could be skipped when porting under to stdlib2.
2019-08-06[ssr] under: extend ssreflect.v to generalize iff to any setoid eqErik Martin-Dorel
* Add an extra test with an Equivalence. * Update the doc accordingly.
2019-08-02Copy edit the Ltac2 documentationTej Chajed
2019-07-29Document changes by PR 10324Vincent Laporte
White spaces are forbidden in the “&ident” syntax for ltac2 references.
2019-07-29Merge PR #10548: Refine documentation of tokensThéo Zimmermann
Reviewed-by: Zimmi48 Ack-by: cpitclaudel Ack-by: herbelin
2019-07-28Update documentation on tokens, use "int" and "num"Jim Fehrle
for integers and natural nums
2019-07-25Remove deprecated `Backtrack` commandMaxime Dénès
It has been deprecated since 8.4. The documentation was incorrect since at least 8.5 (the last two arguments were ignored). `Backtrack m n p` was a synonym for `BackTo m` We also move `BackTo` handling to coqtop, since it is not meant to be part of the document.
2019-07-23doc: Fix a detail in 2 files describing the under tacticErik Martin-Dorel
href: coq/coq#9651
2019-07-11Update doc/sphinx/proof-engine/ssreflect-proof-language.rstFlorent Hivert
Co-Authored-By: Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>
2019-07-10Fixed a few wrong reference and typosFlorent Hivert
2019-06-30Merge PR #10356: Re-add the "Show Goal" command for Prooftree in PG.Emilio Jesus Gallego Arias
Reviewed-by: Zimmi48 Reviewed-by: ejgallego Reviewed-by: gares Ack-by: herbelin Ack-by: jfehrle
2019-06-25Re-add the "Show Goal" command for Prooftree in PG.Jim Fehrle
It prints a goal given its internal goal id and the Stm state id.
2019-06-25Give a functional type to Ltac1 quotations with a context.Pierre-Marie Pédrot
This looks more principled, and doesn't require as much tinkering with the typing implementation.
2019-06-25Documenting the Ltac2 change.Pierre-Marie Pédrot
2019-06-15Rename expr and tacexpr tokens into ltac_expr token family.Théo Zimmermann
This allows to refer to them from other part of the manual without any ambiguity.
2019-06-06[Ltac2] Interpretation scopes in “constr” arguments of tactic notationsVincent Laporte
2019-06-03Merge PR #10277: Remove Show Script (deprecated in 8.10)Théo Zimmermann
Reviewed-by: Zimmi48 Reviewed-by: gares
2019-06-03Update doc to reflect that PG now supports Coq-generated proof diffsJim Fehrle
2019-05-31Remove Show Script (deprecated in 8.10)Gaëtan Gilbert
2019-05-26Merge PR #10220: Use new coqrst syntax for alternatives in SSReflect chapter.Enrico Tassi
Reviewed-by: gares
2019-05-25Documenting syntax "injection ... as [= pat1 ... patn ]".Hugo Herbelin
To prevent confusion, forbidding a mix of the "injection term as pat1 ... patn" and of the "injection term as [= pat1 ... patn]" syntax: If a "[= ...]" occurs, this should be a singleton list of patterns.
2019-05-23Merge PR #10195: Minor Ltac2 documentation fix: type parameters are optional.Clément Pit-Claudel
Reviewed-by: cpitclaudel Reviewed-by: ppedrot
2019-05-23Suggestions from review.Théo Zimmermann
Co-authored-by: Jason Gross <jgross@mit.edu>
2019-05-23More misc refman fixes, less undefined tokens.Théo Zimmermann
2019-05-23Define many undefined tokens, and other misc fixes.Théo Zimmermann
Progress towards #9411, extracted from #10118, rebased ontop of #10192.
2019-05-23Use new coqrst syntax for alternatives in SSReflect chapter.Théo Zimmermann
2019-05-22[refman] Add more missing @ signsClément Pit-Claudel
2019-05-22[refman] Misc fixes (mostly missing '@' signs)Clément Pit-Claudel
Co-Authored-By: @Zimmi48
2019-05-22[refman] Give explicit names to the various 'Arguments' commandsClément Pit-Claudel
2019-05-22Ltac2 doc fix: syntax for extending an open variant type.Théo Zimmermann
2019-05-21Fixing typos - Part 1JPR
2019-05-20Minor Ltac2 documentation fix: type parameters are optional.Théo Zimmermann
2019-05-19[refman] Document etransitivityClément Pit-Claudel
2019-05-19[refman] Misc fixes (indentation, whitespace, notation syntax)Clément Pit-Claudel
2019-05-19Merge PR #10143: Add dedicated syntax for alternatives (abc | def) in manual ↵Théo Zimmermann
notations Reviewed-by: Zimmi48 Ack-by: jfehrle
2019-05-16[refman] Introduce syntax for alternatives in notationsClément Pit-Claudel
Closes GH-8482.
2019-05-12[refman] Use 'flag' instead of 'opt' for 'Ltac2 Debug'Clément Pit-Claudel
2019-05-10Better title for the first example of the Ltac examples section.Théo Zimmermann
2019-05-09Improve the first two Ltac examples.Théo Zimmermann
2019-05-09Rewording, language improvements.Théo Zimmermann
Co-Authored-By: Jim Fehrle <jim.fehrle@gmail.com>
2019-05-08[refman] Move all the Ltac examples to the Ltac chapter.Théo Zimmermann
The Detailed examples of tactics chapter can be removed when the remaining examples are moved closer to the definitions of the corresponding tactics. This commit also moves back the footnotes from the Tactics chapter at the end of the chapter, and removes an old footnote that doesn't matter anymore.
2019-05-07Merge PR #10077: [refman] Add a note reminding about the typeclass_instances ↵Clément Pit-Claudel
database. Reviewed-by: cpitclaudel
2019-05-07Merge PR #10053: Document change_no_check variantsThéo Zimmermann
Ack-by: JasonGross Reviewed-by: Zimmi48
2019-05-07Merge PR #10002: Integrate ltac2Théo Zimmermann
Ack-by: JasonGross Reviewed-by: gares Reviewed-by: ppedrot Reviewed-by: jfehrle Ack-by: SkySkimmer Reviewed-by: Zimmi48 Reviewed-by: ejgallego
2019-05-07[refman] Add a note reminding about the typeclass_instances database.Théo Zimmermann
Closes #10072.
2019-05-07Integrate build and documentation of Ltac2Maxime Dénès
Since Ltac2 cannot be put under the stdlib logical root (some file names would clash), we move it to the `user-contrib` directory, to avoid adding another hardcoded path in `coqinit.ml`, following a suggestion by @ejgallego. Thanks to @Zimmi48 for the thorough documentation review and the numerous suggestions.
2019-05-03Copy-editing from code reviewJason Gross
Co-Authored-By: Blaisorblade <p.giarrusso@gmail.com>
2019-05-03Documentation for change_no_check untested variantsPaolo G. Giarrusso
Copy change's variants in change_no_check, since supposedly they should all be supported. But they haven't been tested, and my example fails.
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 08:56:21 +0000