aboutsummaryrefslogtreecommitdiff
path: root/doc/sphinx/proof-engine
AgeCommit message (Collapse)Author
2020-01-27Rephrase to reduce ambiguityPaolo G. Giarrusso
This is the smallest possible change to clarify the text without making it even more formal.
2020-01-27Fix off-by-one in docs of `first num last` (fix #11463)Paolo G. Giarrusso
2020-01-25Merge PR #11025: Add Set NativeCompute TimingMaxime Dénès
Ack-by: SkySkimmer Reviewed-by: Zimmi48 Ack-by: jfehrle Reviewed-by: maximedenes
2020-01-14Document the Set Default Proof Mode command.Pierre-Marie Pédrot
Fixes #10909: Set Default Proof Mode is not documented.
2020-01-10missing spaceOlivier Laurent
2020-01-08Add Set NativeCompute TimingJason Gross
The command `Set NativeCompute Timing` causes calls to `native_compute` (as well as kernel calls to the native compiler) to emit separate timing information about compilation, execution, and reification. This allows more fine-grained timing of the native compiler without needing to set the `-debug` flag.
2020-01-08Add note about default goal selector next to bullet docsGaëtan Gilbert
Close #11036
2019-12-23Merge PR #11324: [refman] Mention Ltac2 in intro.Pierre-Marie Pédrot
Reviewed-by: jfehrle
2019-12-23Merge PR #10760: Make rapply handle all numbers of underscoresPierre-Marie Pédrot
Ack-by: Zimmi48 Reviewed-by: ppedrot
2019-12-22[refman] Mention Ltac2 in intro.Théo Zimmermann
2019-12-14Fix refine and eapply to mark shelved goals as non-resolvable, alwaysMatthieu Sozeau
Check that we don't regress on PR #10762 example Fix regression discovered by Arthur in PR #10762 Fix script of #10298 which was relying on breaking semantics for `eapply` Add doc Add comment in clenvtac Actually, always mark shelved goals as unresolvable Update doc to reflect semantics w.r.t. shelved subgoals
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-26Remove `rapply` tactic notation in favor of just the tacticJason Gross
This increases backwards compatibility. If desired, we can add a tactic notation to simplify the spec of `rapply` in the future if we want.
2019-11-26Make rapply handle all numbers of underscoresJason Gross
Also add a tactic notation so that it takes in uconstrs by default. Also add some basic tests for `rapply`. Also document rapply in the manual
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-12 01:23:27 +0000