| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2019-11-25 | Minor fix in doc for [unfold] | Gaëtan Gilbert | |
| Close #9634 | |||
| 2019-11-21 | Merge PR #11145: Document -vos flag for coqdep | Emilio Jesus Gallego Arias | |
| Reviewed-by: Zimmi48 Reviewed-by: ejgallego | |||
| 2019-11-21 | Merge PR #10614: Update the Gallina grammar in doc, "Terms" section | Théo Zimmermann | |
| Ack-by: Zimmi48 | |||
| 2019-11-21 | Document -vos flag for coqdep | Gaëtan Gilbert | |
| 2019-11-21 | Merge PR #11075: load .vo when .vos is missing + misc vos changes | Emilio Jesus Gallego Arias | |
| Reviewed-by: gares Reviewed-by: silene | |||
| 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-20 | Merge PR #11119: 8.10-backportable part of #10575 | Clément Pit-Claudel | |
| Reviewed-by: cpitclaudel | |||
| 2019-11-20 | From CoqIDE or -vos or -vok compilation, load .vo when .vos is missing ↵ | charguer | |
| (fixing bug #11057). With this new behavior, it is not needed to .vos files in user contribs. Also, this commit adds a feature: upon creation of a .vo file, an empty .vok file is touched. | |||
| 2019-11-16 | Merge PR #10996: Refine Instance returns | Pierre-Marie Pédrot | |
| Reviewed-by: Zimmi48 Reviewed-by: ejgallego Reviewed-by: ppedrot | |||
| 2019-11-14 | Merge PR #10979: Fix doc for universes(foo) attributes | Théo Zimmermann | |
| Reviewed-by: Zimmi48 | |||
| 2019-11-14 | Fix doc for universes(foo) attributes | Gaëtan Gilbert | |
| Fix #10570 | |||
| 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-14 | Restore documentation of `Typeclasses Axioms Are Instances` | Maxime Dénès | |
| This documentation seems to have been lost after it was introduced by 0ad26633a4589d77de1f864733d1d953dab9ea91 We also document that this flag is deprecated. | |||
| 2019-11-14 | Document recommended syntax for `firstorder` | Maxime Dénès | |
| Only the deprecated one was documentated, and the deprecation was not mentioned. | |||
| 2019-11-13 | Return of Refine Instance as an attribute. | Gaëtan Gilbert | |
| We can now do `#[refine] Instance : Bla := bli.` to enter proof mode with `bli` as a starting refinement. If `bli` is enough to define the instance we still enter proof mode, keeping things nicely predictable for the stm. | |||
| 2019-11-08 | Merge PR #11050: Replace "option" in doc when it refers to a flag | Théo Zimmermann | |
| Reviewed-by: Zimmi48 | |||
| 2019-11-06 | Replace "option" in doc when it refers to a flag | Jim Fehrle | |
| 2019-11-04 | Cite POPL19 SProp paper | Gaëtan Gilbert | |
| Close #10242 | |||
| 2019-11-03 | Elan → Stratego in documentation of `rewrite_strat`. | Robbert Krebbers | |
| @eelcovisser told me that the strategies in Luttik and Visser 97 were inspired by Elan, but they are not part of Elan. They are part of the Stratego language. | |||
| 2019-11-01 | Merge PR #11028: Update the deprecation doc of `Shrink Obligations` | Clément Pit-Claudel | |
| 2019-11-01 | Merge PR #10022: [ssr] Generalize tactics under and over to any (Reflexive) ↵ | Enrico Tassi | |
| relation Reviewed-by: gares | |||
| 2019-11-01 | Update the deprecation doc of `Shrink Obligations` | Jason Gross | |
| Now it uses `.. deprecated` like all the other deprecation notices in the manual. | |||
| 2019-11-01 | Merge PR #9867: Add primitive floats (binary64 floating-point numbers) | Maxime Dénès | |
| Ack-by: SkySkimmer Reviewed-by: Zimmi48 Ack-by: ejgallego Reviewed-by: maximedenes Ack-by: proux01 Ack-by: silene Ack-by: vbgl | |||
| 2019-11-01 | Add warnings regarding the experimental nature of the vos feature in the doc. | Pierre-Marie Pédrot | |
| 2019-11-01 | fix coq_makefile and doc for vos support. | charguer | |
| 2019-11-01 | additional details in the doc for -vos | charguer | |
| 2019-11-01 | Implementing support for vos/vok files. | charguer | |
| A .vos file stores the result of compiling statements (defs, lemmas) but not proofs. A .vok file is an empty file that denotes successful compilation of the full contents of a .v file. Unlike a .vio file, a .vos file does not store suspended proofs, so it is more lightweight. It cannot be completed into a .vo file. | |||
| 2019-11-01 | docs(gallina-extensions.rst): Say more on float literals extraction | Erik Martin-Dorel | |
| 2019-11-01 | docs: Add refman+stdlib documentation | Erik Martin-Dorel | |
| 2019-11-01 | [ssr] Update doc for under w.r.t. setoid-like relations | Erik Martin-Dorel | |
| 2019-10-31 | Merge PR #10985: Print argument info as an Arguments command in About | Emilio Jesus Gallego Arias | |
| Ack-by: Zimmi48 Ack-by: cpitclaudel Reviewed-by: ejgallego | |||
| 2019-10-31 | Merge PR #9883: Add support for Sorts in numeral notations | Vincent Laporte | |
| Ack-by: SkySkimmer Ack-by: proux01 Reviewed-by: vbgl | |||
| 2019-10-31 | Merge PR #10997: Implement the unsupported attribute error using the warning ↵ | Emilio Jesus Gallego Arias | |
| system Reviewed-by: Zimmi48 Reviewed-by: ejgallego | |||
| 2019-10-31 | Doc: index command Arguments with assert | Gaëtan Gilbert | |
| 2019-10-31 | Merge PR #10861: Fix #10615: Notation substitution for Ltac2 terms. | Gaëtan Gilbert | |
| Reviewed-by: SkySkimmer Ack-by: jfehrle | |||
| 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-30 | Use bullets and indentation (but the result rendering is weird). | Théo Zimmermann | |
| 2019-10-30 | Use explicit match as suggested by Clément. | Théo Zimmermann | |
| 2019-10-30 | [refman] Add a second example of contradiction when positivity checking is ↵ | Théo Zimmermann | |
| disabled. | |||
| 2019-10-30 | [refman] Give an example of contradiction when positivity checking is disabled. | Théo Zimmermann | |
| 2019-10-30 | Merge PR #10494: Show diffs in "Show Proof." | Enrico Tassi | |
| Reviewed-by: Zimmi48 Reviewed-by: gares Ack-by: herbelin | |||
| 2019-10-29 | Show 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-29 | Fix #9114, assert_succeeds (exact I) solves goal | Jason Gross | |
| 2019-10-29 | `assert_succeeds`&`assert_fails`: multisuccess fix | Jason Gross | |
| These tactics now work correctly with multisuccess tactics by wrapping the tactic argument in `once`. Fixes #10965 | |||
| 2019-10-29 | Document the ability to bind notation arguments in Ltac2. | Pierre-Marie Pédrot | |
| 2019-10-28 | Add support for Sorts in numeral notations | Jason Gross | |
| 2019-10-24 | Release notes for Coq 8.10.1 | Vincent Laporte | |
| 2019-10-23 | Better wording for "Show Proof" and fix typos | Jim Fehrle | |
| 2019-10-23 | Merge PR #10929: documentation fixes | Théo Zimmermann | |
| Ack-by: Zimmi48 Reviewed-by: jfehrle | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |