| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 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 | Changelog entry | Maxime Dénès | |
| 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 | Add extraction for primitive floats | Erik Martin-Dorel | |
| Co-authored-by: Pierre Roux <pierre.roux@onera.fr> | |||
| 2019-11-01 | docs: Add entry in changelog | 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-11-01 | [ssr] Refactor/Extend of under to support more relations | Erik Martin-Dorel | |
| (namely, [RewriteRelation]s beyond Equivalence ones) Thanks to @CohenCyril for suggesting this enhancement | |||
| 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 | changelog for #10985 | Gaëtan Gilbert | |
| 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-29 | Merge PR #10947: Rename `VDFILE` from `.coqdeps.d` to `.<CoqMakefile>.d` in ↵ | Enrico Tassi | |
| `coq_makefile` Ack-by: SkySkimmer Reviewed-by: gares | |||
| 2019-10-28 | Add support for Sorts in numeral notations | Jason Gross | |
| 2019-10-28 | Merge PR #10963: Possible simplification of parsing rules. | Clément Pit-Claudel | |
| Reviewed-by: ppedrot | |||
| 2019-10-28 | Rename `VDFILE` from `.coqdeps.d` to `.<CoqMakefile>.d` in the ↵ | Kazuhiko Sakaguchi | |
| `coq_makefile` utility The `coq_makefile` utility and `Makefile`s generated by it generate and include some files: `<CoqMakefile>.conf`, `<CoqMakefile>.local`, and the dependency file `.coqdep.d`, where `<CoqMakefile>` is the name of the output file given by the `-o` option. Out of these, only the name of the dependency file `.coqdep.d` is fixed to a constant. This seems to be a potential pitfall when we place multiple `Makefile`s generated by `coq_makefile` in the same directory. This patch renames `.coqdeps.d` to `.<CoqMakefile>.d`. | |||
| 2019-10-28 | Fix typos. | Théo Zimmermann | |
| Co-Authored-By: Clément Pit-Claudel <cpitclaudel@users.noreply.github.com> | |||
| 2019-10-28 | Add changelog for #10963. | Théo Zimmermann | |
| 2019-10-27 | Merge PR #10827: Replace classical reals quotient axioms by functional ↵ | Hugo Herbelin | |
| extensionality Ack-by: JasonGross Ack-by: Zimmi48 Ack-by: herbelin Ack-by: maximedenes | |||
| 2019-10-25 | [declare] Generalize kind type on declareDef | Emilio Jesus Gallego Arias | |
| This is useful to remove some duplicate bits in other declare files. | |||
| 2019-10-24 | Replace classical reals quotient axioms by functional extensionality. Define ↵ | Vincent Semeria | |
| homotopy propositions and homotopy sets. Rename local variable R in test Nsatz, to avoid a name collision with the type of real numbers. | |||
| 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 #10932: Add a notation for the empty type. | Théo Zimmermann | |
| Reviewed-by: Zimmi48 Reviewed-by: amahboubi | |||
| 2019-10-23 | Merge PR #10929: documentation fixes | Théo Zimmermann | |
| Ack-by: Zimmi48 Reviewed-by: jfehrle | |||
| 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-10-22 | Merge PR #10880: Allow to pass Ltac1 values to Ltac2 quotations. | Jason Gross | |
| Ack-by: SkySkimmer Reviewed-by: Zimmi48 | |||
| 2019-10-22 | Update doc/changelog/06-ssreflect/10932-void-type-ssr.rst | Arthur Azevedo de Amorim | |
| Improve changelog. Co-Authored-By: Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | |||
| 2019-10-22 | Update changelog. | Arthur Azevedo de Amorim | |
| 2019-10-22 | Merge PR #10899: Fixes #10894 regression: uconstr was not anymore typed in ↵ | Pierre-Marie Pédrot | |
| the Ltac-substituted environment Reviewed-by: ejgallego Reviewed-by: ppedrot | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |