| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 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" | |||
| 2019-01-18 | [ssr] compile "=> {} y" as "=> {y} y" | Enrico Tassi | |
| 2018-12-19 | [doc] typo | Enrico Tassi | |
| 2018-12-18 | [ssr] make > a stand alone intro pattern | Enrico Tassi | |
| 2018-12-18 | [ssr] extended intro patterns: + > [^] /ltac: | Enrico Tassi | |
| This commit implements the following intro patterns: Temporary "=> +" "move=> + stuff" ==== "move=> tmp stuff; move: tmp" It preserves the original name. "=>" can be chained to force generalization as in "move=> + y + => x z" Tactics as views "=> /ltac:(tactic)" Supports notations, eg "Notation foo := ltac:(bla bla bla). .. => /foo". Limited to views on the right of "=>", views that decorate a tactic as move or case are not supported to be tactics. Dependent "=> >H" move=> >H ===== move=> ???? H, with enough ? to name H the first non-dependent assumption (LHS of the first arrow). TC isntances are skipped. Block intro "=> [^ H] [^~ H]" after "case" or "elim" or "elim/v" it introduces in one go all new assumptions coming from the eliminations. The names are picked from the inductive type declaration or the elimination principle "v" in "elim/v" and are appended/prepended the seed "H" The implementation makes crucial use of the goal_with_state feature of the tactic monad. For example + schedules a generalization to be performed at the end of the intro pattern and [^ .. ] reads the name seeds from the state (that is filled in by case and elim). | |||
| 2018-12-14 | Fix the SSReflect chapter regarding objects without bodies. | Théo Zimmermann | |
| 2018-12-04 | Add undocumented options from mattam82 | Jim Fehrle | |
| 2018-12-04 | Document undocumented flags and options | Jim Fehrle | |
| Also remove a few undocumented settings | |||
| 2018-10-24 | [Manual] Prevent an irrelevant warning to show up | Vincent Laporte | |
| 2018-10-24 | [Manual] Avoid using deprecated “Focus” | Vincent Laporte | |
| 2018-10-24 | [Manual] Fix rendering of an example | Vincent Laporte | |
| 2018-10-24 | [Manual] Typo | Vincent Laporte | |
| 2018-10-24 | [Manual] Fix an example | Vincent Laporte | |
| The `Undo` command is not reliable. | |||
| 2018-10-24 | [Manual] Fix layout of a list | Vincent Laporte | |
| 2018-09-20 | Rewrite "Flags, Options and Tables" section. | Jim Fehrle | |
| Mark boolean-valued options with :flag: Adjust tactic and command names so parameters aren't shown in the index unless they're needed for disambiguation. Remove references to synchronous options. Revise doc for tables. Correct indentation for text below :flag: | |||
| 2018-09-20 | [doc] Include the rst and LaTeX preambles automatically in all files | Clément Pit-Claudel | |
| 2018-09-11 | Grammar entry for the ssr syntax for anonymous arguments. | Assia Mahboubi | |
| 2018-08-31 | Uniformized many spelling variants. Added .. warning:: and .. seealso:: ↵ | Zeimer | |
| directives in many places. Disambiguated terminology: disequality now means <> while inequality means < <= > >=. Fixed some more grammar and spelling issues. | |||
| 2018-08-29 | [sphinx] Fix timeout issue by splitting imports. | Théo Zimmermann | |
| 2018-07-30 | [sphinx] Use arguments of '.. example::' directive as a title | Clément Pit-Claudel | |
| Most existing uses of .. example did not use the first line as a title, so this commit also adds appropriate blank lines. | |||
| 2018-06-22 | [ssr] document {}/view | Enrico Tassi | |
| 2018-06-22 | [ssr] document rewrite {}foo | Enrico Tassi | |
| It was used in some examples, but never fully documented | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |