| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2020-06-08 | Convert Ltac chapter to prodn | Jim Fehrle | |
| 2020-06-08 | Make automatic name generation for directives more consistent: | Jim Fehrle | |
| - by default, generate names for all directives using the prefix "[a-zA-Z0-9_ ]+" except - don't generate a name for cmdv and tacv - generate more flexibily for exn, warn and attr | |||
| 2020-05-15 | Document new Search features. | Théo Zimmermann | |
| 2020-05-01 | Fixing #11903: Fixpoints not truly recursive in standard library. | Hugo Herbelin | |
| There was also a non truly recursive in the doc. | |||
| 2020-04-23 | [documentation] ssreflect: Abbreviations do not support scope | Kenji Maillard | |
| 2020-04-17 | Deprecate “omega” | Vincent Laporte | |
| 2020-02-28 | Convert Gallina Vernac to use prodn | Jim Fehrle | |
| 2020-01-27 | Rephrase to reduce ambiguity | Paolo G. Giarrusso | |
| This is the smallest possible change to clarify the text without making it even more formal. | |||
| 2020-01-27 | Fix off-by-one in docs of `first num last` (fix #11463) | Paolo G. Giarrusso | |
| 2019-11-14 | Merge PR #11100: small documentation fixes | Théo Zimmermann | |
| Reviewed-by: Zimmi48 Ack-by: cpitclaudel | |||
| 2019-11-14 | doc fixes | Antonio Nikishaev | |
| 2019-11-06 | Replace "option" in doc when it refers to a flag | Jim Fehrle | |
| 2019-11-01 | Merge 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 relations | Erik Martin-Dorel | |
| 2019-10-23 | Better wording for "Show Proof" and fix typos | Jim Fehrle | |
| 2019-10-22 | documentation fixes | Antonio Nikishaev | |
| document « Property » more documentation fixes [doc] destructed → destructured [doc] another le_minus→lt_1_r [doc] @jfehrle suggestions [doc] more minor fixes | |||
| 2019-08-08 | [ssr] Refactor under's Setoid generalization to ease stdlib2 porting | Erik 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 eq | Erik Martin-Dorel | |
| * Add an extra test with an Equivalence. * Update the doc accordingly. | |||
| 2019-07-23 | doc: Fix a detail in 2 files describing the under tactic | Erik Martin-Dorel | |
| href: coq/coq#9651 | |||
| 2019-07-11 | Update doc/sphinx/proof-engine/ssreflect-proof-language.rst | Florent Hivert | |
| Co-Authored-By: Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | |||
| 2019-07-10 | Fixed a few wrong reference and typos | Florent Hivert | |
| 2019-05-26 | Merge PR #10220: Use new coqrst syntax for alternatives in SSReflect chapter. | Enrico Tassi | |
| Reviewed-by: gares | |||
| 2019-05-23 | Define many undefined tokens, and other misc fixes. | Théo Zimmermann | |
| Progress towards #9411, extracted from #10118, rebased ontop of #10192. | |||
| 2019-05-23 | Use new coqrst syntax for alternatives in SSReflect chapter. | Théo Zimmermann | |
| 2019-05-22 | [refman] Add more missing @ signs | Clément Pit-Claudel | |
| 2019-05-21 | Fixing typos - Part 1 | JPR | |
| 2019-05-19 | [refman] Misc fixes (indentation, whitespace, notation syntax) | Clément Pit-Claudel | |
| 2019-05-16 | [refman] Introduce syntax for alternatives in notations | Clément Pit-Claudel | |
| Closes GH-8482. | |||
| 2019-04-23 | [ssr] under: optimization of the tactic for (under eq_bigl => *) | Erik Martin-Dorel | |
| so it acts "more naturally" like (under eq_bigl; [hnf|]); move=> [*|]. Also: replace "by over." in the doc example with "over." | |||
| 2019-04-23 | [ssr] Define over as a rewrite rule & Merge 'Under[ _ ] notations | Erik Martin-Dorel | |
| as suggested by @gares, and: * Rename some Under_* terms for better uniformity; * Update & Improve minor details in the documentation. | |||
| 2019-04-23 | [doc] ssr_under: a few improvements | Enrico Tassi | |
| 2019-04-23 | [ssr] under: Fix the defective form ("=> [*|*]" implied) and its doc | Erik Martin-Dorel | |
| * Add tests accordingly. | |||
| 2019-04-23 | [ssr] under: Fix and extend the documentation | Erik Martin-Dorel | |
| 2019-04-23 | [ssr] new syntax for the under tactic | Enrico Tassi | |
| 2019-04-23 | [ssr] under: Add doc for {under, over} & Add entry in CHANGES.md | Erik Martin-Dorel | |
| * For better uniformity, replace "intro-pattern" with "intro pattern" in the ssr doc. | |||
| 2019-03-10 | Merge PR #9654: [sphinx] Add warn option to coqtop directive. | Clément Pit-Claudel | |
| Ack-by: SkySkimmer Ack-by: Zimmi48 Ack-by: vbgl Reviewed-by: cpitclaudel | |||
| 2019-03-01 | [doc] ssr: Fix the documentation of `by [tacs]` | Erik Martin-Dorel | |
| Closes coq/coq#9669 | |||
| 2019-02-28 | [sphinx] Add warn option to coqtop directive. | Théo Zimmermann | |
| By default Coq warnings are made fatal when building the manual. If you want to show a command resulting in a warning, use the warn option. Preexisting warnings are either fixed or marked as expected. | |||
| 2019-02-19 | [sphinx] Refactor handling of options for coqtop directive. | Théo Zimmermann | |
| Make it mandatory to give exactly one display option. | |||
| 2019-02-18 | Using options abort and restart of coqtop directive in the manual. | Théo Zimmermann | |
| 2019-02-18 | Fix last nested lemma failure. | Théo Zimmermann | |
| 2019-02-14 | [Manual] Don’t use `Undo` in ssreflect examples | Vincent Laporte | |
| 2019-02-12 | Fix failing coqtops in ssreflect-proof-language.rst | Gaëtan Gilbert | |
| 2019-01-24 | [doc] warn that (automatic) clears can result in errors | Enrico Tassi | |
| 2019-01-24 | [doc] more precise description of when automatic clears are triggered | Enrico Tassi | |
| 2019-01-24 | [doc] explain how to avoid automatic clears | Enrico Tassi | |
| 2019-01-22 | clarify when an ident is added to the clear switch | Enrico Tassi | |
| 2019-01-22 | Apply suggestions from code review | Théo Zimmermann | |
| Co-Authored-By: gares <gares@fettunta.org> | |||
| 2019-01-21 | [ssr] better structure the ipats doc | Enrico Tassi | |
| 2019-01-19 | [ssr] compile "=> {x..} y" as "=> {x..y} y" | Enrico Tassi | |
| This is for consistency with "rewrite {x..} y" | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |