| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2020-05-16 | Add redirects for HTML pages that were moved. | Théo Zimmermann | |
| 2020-05-13 | Create a new file on Variants. | Théo Zimmermann | |
| 2020-05-13 | Extract Variants from Gallina. | Théo Zimmermann | |
| 2020-05-01 | Move essential vocabulary and syntax conventions to section on basics. | Théo Zimmermann | |
| 2020-05-01 | Remove lexical conventions and attributes from Gallina chapter. | Théo Zimmermann | |
| 2020-04-26 | Convert syntax extensions chapter to prodn | Jim Fehrle | |
| 2020-04-10 | Convert vernac commands chapter to prodn, update syntax | Jim Fehrle | |
| 2020-03-26 | Merge PR #11877: Removing deprecated destruct/remember syntax _eqn. | Théo Zimmermann | |
| Reviewed-by: Zimmi48 | |||
| 2020-03-26 | Removing deprecated destruct syntax _eqn. | Hugo Herbelin | |
| 2020-03-25 | Doc_grammar: Update cmd:: and tacn:: constructs in .rsts | Jim Fehrle | |
| Remove unneeded source and output files Move all commands under command NT Add a lot of edits for commands and tactics | |||
| 2020-03-25 | Convert Gallina Extensions to use prodn | Jim Fehrle | |
| 2020-03-19 | Document all the existing attributes. | Théo Zimmermann | |
| And fix documentation following the removal of the Template Check flag in #11546. | |||
| 2020-03-09 | Remove some productionlists | Jim Fehrle | |
| 2020-02-28 | Convert Gallina Vernac to use prodn | Jim Fehrle | |
| 2020-02-17 | New syntax [Inductive Acc A R | x : Prop := ...] | Gaëtan Gilbert | |
| to control uniform parameters. This replaces the attribute. | |||
| 2020-02-17 | Revert "Add #[uniform] and #[nonuniform] (for Uniform Inductive Parameters)" | Gaëtan Gilbert | |
| This reverts commit bc2c1836ba4c878903288060bcb66a0ef1aaced6. | |||
| 2020-02-13 | Add #[uniform] and #[nonuniform] (for Uniform Inductive Parameters) | Gaëtan Gilbert | |
| 2020-02-04 | Update doc for non max implicit arguments | SimonBoulier | |
| 2020-01-09 | Merge PR #11164: [CS] allow Let variable to be canonical | Pierre-Marie Pédrot | |
| Ack-by: SkySkimmer Ack-by: Zimmi48 Ack-by: ejgallego Reviewed-by: ppedrot | |||
| 2020-01-06 | Merge PR #11340: [refman] Fix bad quoting practice leftover from Sphinx ↵ | Clément Pit-Claudel | |
| migration. Reviewed-by: jfehrle | |||
| 2019-12-31 | Merge PR #11325: [refman] Add missing s. | Pierre-Marie Pédrot | |
| Reviewed-by: jfehrle | |||
| 2019-12-29 | Remove :flag: that appears in the output | Jim Fehrle | |
| 2019-12-29 | [refman] Fix bad quoting practice leftover from Sphinx migration. | Théo Zimmermann | |
| 2019-12-28 | Convert productionlists to prodns | Jim Fehrle | |
| 2019-12-24 | [Attributes] accept #[canonical] (Let|Definition) | Enrico Tassi | |
| 2019-12-22 | [refman] Add missing s. | Théo Zimmermann | |
| 2019-11-20 | Update grammar in the Terms section of Gallina chapter | Jim 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-14 | Fix doc for universes(foo) attributes | Gaëtan Gilbert | |
| Fix #10570 | |||
| 2019-11-06 | Replace "option" in doc when it refers to a flag | Jim Fehrle | |
| 2019-10-30 | Implement the unsupported attribute error using the warning system | Gaëtan Gilbert | |
| This means we can disable it to ignore unsupported attributes. For instance this would be useful if we change some behaviour of `Cmd` and add an attribute `att` to restore the old behaviour, then `#[att] Cmd` is backwards compatible if the warning is disabled. | |||
| 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-16 | Add documentation for typing flags. | SimonBoulier | |
| 2019-07-28 | Update documentation on tokens, use "int" and "num" | Jim Fehrle | |
| for integers and natural nums | |||
| 2019-06-06 | `deprecated` attribute support for notations and syntactic definitions | Maxime Dénès | |
| We also slightly change the semantics of the `compat` syntax modifier to re-express it in terms of the `deprecated` attribute, and we deprecate it in favor of the latter. | |||
| 2019-05-23 | do not parse `|` as infix in patterns; parse `|}` as `|` `}` | Georges Gonthier | |
| * use mixfix `(p1 | … | pn)` notation for nested disjunctive patterns, rather than infix `|`, making pattern syntax consistent with term syntax. * disable extending `pattern` grammar with notation incompatible with the nested disjunctive pattern syntax `(p1 | … | pn)`, such as the `(p | q)` divisibility notation used by `Numbers`. * emit a (disabled by default) `disj-pattern-notation` warning when such `Notation` is attempted. * update documentation accordingly; document incompatibilities in `changelog`. * comment special treatment of `(num)` in grammar. * update file extensions in `Pcoq` header comment. * correct the keyword declarations to reflect the contents of the grammar files; perhaps there should be an option to disable implicit keyword extension in a `.mlg` file, so that these lists could actually be checked. * parse the `|}` manifest record terminator as `|` followed by `}`, eliminating the `|}` token which conflicts with notations that use `|` as a terminator (such as, absolute value, norm, or cardinal in MathComp). Since `|` is now an `operconstr` _and_ `pattern` terminator, `bar_cbrace` rule checks for contiguous symbols, this change entails no visible behaviour change. | |||
| 2019-05-19 | [refman] Misc fixes (indentation, whitespace, notation syntax) | Clément Pit-Claudel | |
| 2019-04-02 | Allow underscores as comments in numeral constants. | Pierre Roux | |
| The numerals lexed are now [0-9][0-9_]* ([.][0-9_]+)? ([eE][+-]?[0-9][0-9_]*)? | |||
| 2019-04-02 | Update documentation | Pierre Roux | |
| 2019-03-18 | [Manual] Parametrize -> ParametErize | Lysxia | |
| - Refine some `@term` into `@type` | |||
| 2019-03-18 | [Manual] Move command Context after Let, and more polishing | Lysxia | |
| - Refine some `@term` into `@type` | |||
| 2019-03-17 | [Manual] Move doc on Let into Section mechanism, and more polishing | Lysxia | |
| - Put "Section mechanism" example earlier | |||
| 2019-03-17 | [Manual] Gather section-specific commands in Section documentation (fix #9704) | Lysxia | |
| 2019-03-17 | [Manual] Improve chapter Type classes, and add mention of Context under Variable | Lysxia | |
| - More consistent code indentation - Nest command variants properly - Make `Context` explanation a bit less terse, with more links - Typesetting bits, add some :cmd: links | |||
| 2019-03-14 | Documentation for SProp | Gaëtan Gilbert | |
| 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-12 | Fix failing coqtops in gallina-specification-language.rst | Gaëtan Gilbert | |
| 2019-01-22 | Remove unneeded | in productionlists | Jim Fehrle | |
| 2018-12-19 | Fix typo in gallina specification language doc | yudetamago | |
| 2018-10-16 | Document the issue with positive coinductive types. | Pierre-Marie Pédrot | |
| 2018-09-28 | Small fixes in attribute documentation. | Théo Zimmermann | |
| In particular, move the footnotes back to the foot of the chapter. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |