aboutsummaryrefslogtreecommitdiff
path: root/doc/sphinx/proof-engine
AgeCommit message (Collapse)Author
2021-04-21Merge PR #14094: Properly pass the Ltac2 notation level to the gramlib API.coqbot-app[bot]
Reviewed-by: JasonGross Ack-by: jfehrle
2021-04-19Merge PR #13815: Improve description of conversionscoqbot-app[bot]
Reviewed-by: Zimmi48 Ack-by: JasonGross
2021-04-17Disambiguate move tactics.Jim Fehrle
2021-04-17Properly pass the Ltac2 notation level to the gramlib API.Pierre-Marie Pédrot
For some reason I was confusing the position and the level in the previous version of the code. Fixes #11866: Ltac2 Notations do not respect precedence.
2021-04-16Merge PR #13939: Allow scope delimiters in Ltac2 open_constr:(...) quotation.coqbot-app[bot]
Reviewed-by: JasonGross
2021-04-02Remove the omega tactic and related optionsJim Fehrle
2021-03-23Merge PR #13774: Allow to register deprecation status in Ltac2 term and ↵Michael Soegtrop
notation declarations Reviewed-by: JasonGross Reviewed-by: Zimmi48 Ack-by: jfehrle
2021-03-13Documenting the changes.Pierre-Marie Pédrot
2021-03-10Add documentation.Pierre-Marie Pédrot
2021-03-10Regenerate the Ltac2 syntax for documentation.Pierre-Marie Pédrot
2021-03-08Convert 2nd part of rewriting chapter to prodnJim Fehrle
2021-02-24Infrastructure for fine-grained debug flagsMaxime Dénès
2021-02-08Properly document the local and global locality attributes.Théo Zimmermann
2021-01-28Merge PR #13763: Remove the SearchHead command (deprecated in 8.12)coqbot-app[bot]
Reviewed-by: SkySkimmer Reviewed-by: Zimmi48
2021-01-25Remove the SearchHead commandJim Fehrle
2021-01-24Merge PR #13762: Remove double induction tacticPierre-Marie Pédrot
Ack-by: Zimmi48 Reviewed-by: ppedrot
2021-01-22Merge PR #13754: Improve doc of occurrences and rewrite.coqbot-app[bot]
Reviewed-by: Zimmi48
2021-01-22Improve doc of occurrences and rewrite.Jim Fehrle
2021-01-20Remove double induction tacticJim Fehrle
2021-01-19Merge PR #13725: Support locality attributes for Hint Rewrite (including export)Pierre-Marie Pédrot
Ack-by: Zimmi48 Ack-by: gares Reviewed-by: ppedrot
2021-01-18Support locality attributes for Hint Rewrite (including export)Gaëtan Gilbert
We deprecate unspecified locality as was done for Hint. Close #13724
2021-01-18Merge PR #13574: Simplistic patch to fix #10113: turn Ltac2's `pattern:` ↵Pierre-Marie Pédrot
into `pat:` Ack-by: Zimmi48 Reviewed-by: jfehrle Reviewed-by: ppedrot
2021-01-07Use nat_or_var for fail/gfailJim Fehrle
2021-01-01Merge PR #13470: Convert rewriting and proof-mode chapters to prodncoqbot-app[bot]
Reviewed-by: Zimmi48 Ack-by: JasonGross
2020-12-30Convert rewriting and proof-mode chapters to prodnJim Fehrle
2020-12-29[refman] Clarify meaning of goal in documentation of instantiate.Théo Zimmermann
2020-12-13Removing flag "Bracketing Last Introduction Pattern".Hugo Herbelin
2020-12-04turn Ltac2's `pattern:` into `pat:`Kenji Maillard
2020-11-26[attributes] [typing] Rename `typing` to `bypass_check`Emilio Jesus Gallego Arias
As discussed in the Coq meeting.
2020-11-26[attributes] [doc] Documentation review by Théo.Emilio Jesus Gallego Arias
Co-authored-by: <Théo Zimmermann <theo.zimmermann@inria.fr>
2020-11-26[vernac] Allow to control typing flags with attributes.Emilio Jesus Gallego Arias
The syntax is the one of boolean attributes, that is to say `#[typing($flag={yes,no}]` where `$flag` is one of `guarded`, `universes`, `positive`. We had to instrument the pretyper in a few places, it is interesting that it is doing so many checks.
2020-11-24Convert auto chapter to prodnJim Fehrle
2020-11-23Merge PR #13417: Use nat_or_var in grammar where negative values don't make ↵coqbot-app[bot]
sense Reviewed-by: Zimmi48
2020-11-20Use nat_or_var where negative values don't make senseJim Fehrle
2020-11-20Granting #9816: apply in takes several hypotheses.Hugo Herbelin
2020-11-14Distinguish one_pattern and one_term nonterminalsJim Fehrle
2020-11-12Merge PR #13345: Addressing #13344: clarifying the role of Add ML Path vs -Icoqbot-app[bot]
Reviewed-by: ejgallego Reviewed-by: Zimmi48 Ack-by: ppedrot Ack-by: jfehrle
2020-11-12Clarifying the role of Add ML Path vs -I (see #13344).Hugo Herbelin
Co-authored-by: Jim Fehrle <jim.fehrle@gmail.com>
2020-11-12Merge PR #13317: [ssr] intro pattern extensions for dup, swap and applycoqbot-app[bot]
Reviewed-by: gares Ack-by: Zimmi48
2020-11-10Convert logic.rst to prodnJim Fehrle
2020-11-09Add global version of OPTINREFJim Fehrle
2020-11-09Merge PR #13329: [refman] Stop applying a special style to Coq, CoqIDE, ↵coqbot-app[bot]
OCaml and Gallina. Reviewed-by: jfehrle Reviewed-by: cpitclaudel
2020-11-09[refman] Stop applying a special style to Coq, CoqIDE, OCaml and Gallina.Théo Zimmermann
The smallcaps rendering was inexistent in the PDF version and did not look good in the HTML version.
2020-11-09Fix #5226: Add index entry for ::=.Théo Zimmermann
2020-11-09Fix indentation of todo in Ltac chapter.Théo Zimmermann
Actual documentation was interpreted as a comment.
2020-11-06Intro pattern extensions for dup, swap and applyCyril Cohen
2020-11-05Add a redirection from previous location of the proof handling chapter.Théo Zimmermann
2020-11-05Various fixes.Théo Zimmermann
2020-11-05Merge content from two origins into the same file.Théo Zimmermann
2020-11-05Move proof handling chapter in new location.Théo Zimmermann
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 11:38:05 +0000