aboutsummaryrefslogtreecommitdiff
path: root/doc/sphinx/proof-engine
AgeCommit message (Collapse)Author
2019-11-30Actually deprecate the `cutrewrite` tacticMaxime Dénès
The manual was already saying that it was deprecated, but no warning was emitted. Fixes #10572
2019-11-30Deprecation annotation for `convert_concl_no_check`Maxime Dénès
2019-11-25Minor fix in doc for [unfold]Gaëtan Gilbert
Close #9634
2019-11-21Merge PR #10614: Update the Gallina grammar in doc, "Terms" sectionThéo Zimmermann
Ack-by: Zimmi48
2019-11-20Update grammar in the Terms section of Gallina chapterJim Fehrle
Update doc_grammar tool The grammar in the doc is generated semi-automatically with doc_grammar: - the grammar is automatically extracted from the mlg files - developer-prepared editing scripts *.mlg_edit modify the extracted grammar for clarity, simplicity and ordering of productions - chunks of the resulting grammar are automatically inserted into the rsts using instructions embedded in the rsts Running doc_grammar is currently a manual step. The grammar updates in the rst files have been manually reviewed.
2019-11-20Merge PR #11119: 8.10-backportable part of #10575Clément Pit-Claudel
Reviewed-by: cpitclaudel
2019-11-14Merge PR #11100: small documentation fixesThéo Zimmermann
Reviewed-by: Zimmi48 Ack-by: cpitclaudel
2019-11-14doc fixesAntonio Nikishaev
2019-11-14Document recommended syntax for `firstorder`Maxime Dénès
Only the deprecated one was documentated, and the deprecation was not mentioned.
2019-11-06Replace "option" in doc when it refers to a flagJim Fehrle
2019-11-01Merge PR #10022: [ssr] Generalize tactics under and over to any (Reflexive) ↵Enrico Tassi
relation Reviewed-by: gares
2019-11-01[ssr] Update doc for under w.r.t. setoid-like relationsErik Martin-Dorel
2019-10-31Merge PR #10861: Fix #10615: Notation substitution for Ltac2 terms.Gaëtan Gilbert
Reviewed-by: SkySkimmer Ack-by: jfehrle
2019-10-30Merge PR #10494: Show diffs in "Show Proof."Enrico Tassi
Reviewed-by: Zimmi48 Reviewed-by: gares Ack-by: herbelin
2019-10-29Show diffs in "Show Proof."Jim Fehrle
Add experimental "Show Proof" command to the toplevel that shadows the current command in the parser (in coqtop and PG only). Apply existing code to highlight diffs in the output
2019-10-29Fix #9114, assert_succeeds (exact I) solves goalJason Gross
2019-10-29`assert_succeeds`&`assert_fails`: multisuccess fixJason Gross
These tactics now work correctly with multisuccess tactics by wrapping the tactic argument in `once`. Fixes #10965
2019-10-29Document the ability to bind notation arguments in Ltac2.Pierre-Marie Pédrot
2019-10-23Better wording for "Show Proof" and fix typosJim Fehrle
2019-10-23Merge PR #10929: documentation fixesThéo Zimmermann
Ack-by: Zimmi48 Reviewed-by: jfehrle
2019-10-22documentation fixesAntonio Nikishaev
document « Property » more documentation fixes [doc] destructed → destructured [doc] another le_minus→lt_1_r [doc] @jfehrle suggestions [doc] more minor fixes
2019-10-18Allow to pass Ltac1 values to Ltac2 quotations.Pierre-Marie Pédrot
This is the dual of #10344.
2019-10-11Merge PR #10489: Fix output for "Printing Dependent Evars Line"Hugo Herbelin
Reviewed-by: Zimmi48 Reviewed-by: ejgallego Ack-by: hendriktews Reviewed-by: herbelin Ack-by: mattam82
2019-10-05Merge PR #10763: Fix syntax of reduction tactics when listing qualid to ↵Vincent Laporte
reduce or not. Reviewed-by: jfehrle
2019-10-04Improve language.Théo Zimmermann
Co-Authored-By: Jim Fehrle <jim.fehrle@gmail.com>
2019-10-04[Stdlib] OrderedType: do not pollute the “core” hint databaseVincent Laporte
2019-09-19Fix #10420 Add dependent evar mapping info to outputJim Fehrle
2019-09-18Fix syntax of reduction tactics when listing qualid to reduce or not.Théo Zimmermann
2019-09-03Add missing index for From ... Require ...Théo Zimmermann
2019-08-16Universe Checking instead of Universes CheckingSimonBoulier
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-27 19:15:48 +0000