aboutsummaryrefslogtreecommitdiff
path: root/doc/sphinx/proof-engine
AgeCommit message (Expand)Author
2019-11-30Actually deprecate the `cutrewrite` tacticMaxime Dénès
2019-11-30Deprecation annotation for `convert_concl_no_check`Maxime Dénès
2019-11-25Minor fix in doc for [unfold]Gaëtan Gilbert
2019-11-21Merge PR #10614: Update the Gallina grammar in doc, "Terms" sectionThéo Zimmermann
2019-11-20Update grammar in the Terms section of Gallina chapterJim Fehrle
2019-11-20Merge PR #11119: 8.10-backportable part of #10575Clément Pit-Claudel
2019-11-14Merge PR #11100: small documentation fixesThéo Zimmermann
2019-11-14doc fixesAntonio Nikishaev
2019-11-14Document recommended syntax for `firstorder`Maxime Dénès
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) r...Enrico Tassi
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
2019-10-30Merge PR #10494: Show diffs in "Show Proof."Enrico Tassi
2019-10-29Show diffs in "Show Proof."Jim Fehrle
2019-10-29Fix #9114, assert_succeeds (exact I) solves goalJason Gross
2019-10-29`assert_succeeds`&`assert_fails`: multisuccess fixJason Gross
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
2019-10-22documentation fixesAntonio Nikishaev
2019-10-18Allow to pass Ltac1 values to Ltac2 quotations.Pierre-Marie Pédrot
2019-10-11Merge PR #10489: Fix output for "Printing Dependent Evars Line"Hugo Herbelin
2019-10-05Merge PR #10763: Fix syntax of reduction tactics when listing qualid to reduc...Vincent Laporte
2019-10-04Improve language.Théo Zimmermann
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 involv...Maxime Dénès
2019-08-08[ssr] Refactor under's Setoid generalization to ease stdlib2 portingErik Martin-Dorel
2019-08-06[ssr] under: extend ssreflect.v to generalize iff to any setoid eqErik Martin-Dorel
2019-08-02Copy edit the Ltac2 documentationTej Chajed
2019-07-29Document changes by PR 10324Vincent Laporte
2019-07-29Merge PR #10548: Refine documentation of tokensThéo Zimmermann
2019-07-28Update documentation on tokens, use "int" and "num"Jim Fehrle
2019-07-25Remove deprecated `Backtrack` commandMaxime Dénès
2019-07-23doc: Fix a detail in 2 files describing the under tacticErik Martin-Dorel
2019-07-11Update doc/sphinx/proof-engine/ssreflect-proof-language.rstFlorent Hivert
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
2019-06-25Re-add the "Show Goal" command for Prooftree in PG.Jim Fehrle
2019-06-25Give a functional type to Ltac1 quotations with a context.Pierre-Marie Pédrot
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
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
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-02-01 18:30:49 +0000