| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2019-11-21 | Document -vos flag for coqdep | Gaëtan Gilbert | |
| 2019-11-21 | Update ↵ | Hugo Herbelin | |
| doc/changelog/02-specification-language/11132-master+fix-implicit-let-fixpoint-bug3282.rst Co-Authored-By: Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | |||
| 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-21 | Taking @Zimmi48's comment into account | Cyril Cohen | |
| Co-Authored-By: Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | |||
| 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-19 | Fixing bugs in the computation of implicit arguments for fix with a let binder. | Hugo Herbelin | |
| 2019-11-19 | coq_makefile: support COQBIN with no ending / | Gaëtan Gilbert | |
| Close #6460 | |||
| 2019-11-19 | added changelog entry | Cyril Cohen | |
| 2019-11-16 | Merge PR #10996: Refine Instance returns | Pierre-Marie Pédrot | |
| Reviewed-by: Zimmi48 Reviewed-by: ejgallego Reviewed-by: ppedrot | |||
| 2019-11-15 | Update doc/changelog/04-tactics/10998-zify-complements.rst | Kazuhiko Sakaguchi | |
| Co-Authored-By: Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | |||
| 2019-11-15 | Add missing zify class instances | Kazuhiko Sakaguchi | |
| Add missing zify class instances for `Pos.pred_double`, `Pos.pred_N`, `Pos.of_nat`, `Pos.add_carry`, `Pos.pow`, `Pos.square`, `Z.pow`, `Z.double`, `Z.pred_double`, `Z.succ_double`, `Z.square`, `Z.div2`, `Z.quot2`, `isZero`, and `isLeZero`. Instances for `isZero` and `isLeZero` are useful to provide new zify instances by using Micromega tactics. | |||
| 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-11 | Run update-compat script with --release option. | Théo Zimmermann | |
| This should ideally have been done before the 8.11 branching. | |||
| 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 | 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. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |