| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-06-22 | Fix handling of universe context for expanded program obligations. | Matthieu Sozeau | |
| The universe context was dropped even though it isn't added to the global universes yet. Keep it so that it is properly defined with the constant the expanded obligation appears in. | |||
| 2018-06-21 | Merge PR #7774: [build] Fix checks and notes noting 4.02.1 instead of 4.02.3 | Maxime Dénès | |
| 2018-06-21 | Merge PR #7873: Make Clément the secondary codeowner of doc/tools/coqrst. | Maxime Dénès | |
| 2018-06-21 | Merge PR #7770: Move indices on top on the TOC. Closes #7764. | Maxime Dénès | |
| 2018-06-21 | Merge PR #7815: On cygwin, pass the filename in a format that coqdoc ↵ | Maxime Dénès | |
| understands. | |||
| 2018-06-21 | Merge PR #7865: Fix #7432: Grammar token @term points to the SSR chapter. | Maxime Dénès | |
| 2018-06-21 | Merge PR #7842: Fix #7836: tools/inferior-coq.el uses next-line instead of ↵ | Pierre Courtieu | |
| forward-line. | |||
| 2018-06-21 | Merge PR #7880: Clean up Dyn | Pierre-Marie Pédrot | |
| 2018-06-21 | Add documentation for Dyn. | whitequark | |
| 2018-06-21 | Rename Dyn.TParam→ValueS, Dyn.MapS.obj→value to clarify their purpose. | whitequark | |
| 2018-06-21 | Reformat Dyn.{ml,mli}. | whitequark | |
| 2018-06-20 | On cygwin, pass the filename in a format that coqdoc understands. | Jim Fehrle | |
| 2018-06-20 | Merge PR #7868: [coqtop] Give priority to stdlib load path over current ↵ | Emilio Jesus Gallego Arias | |
| directory | |||
| 2018-06-20 | Make Clément the secondary codeowner of doc/tools/coqrst. | Théo Zimmermann | |
| 2018-06-19 | [coqtop] Give priority to stdlib load path over current directory | Maxime Dénès | |
| When initilazing the load path, coqtop adds implicit bindings for stdlib and for the current directory (-R stdlib Coq -R . ""). In case of a clash, the binding of the current directory had priority, which makes it impossible to edit stdlib files (when they Require files from the same directory) using PG, or from CoqIDE when launched from the directory containing the file. Example to reproduce the problem: ``` cd plugins/omega coqide Omega.v ``` some of the Requires will fail. | |||
| 2018-06-19 | Merge PR #7797: Remove reference name type. | Enrico Tassi | |
| 2018-06-19 | Merge PR #6754: Better elaboration of pattern-matchings on primitive projections | Pierre-Marie Pédrot | |
| 2018-06-19 | Merge PR #7491: Fix #7421: constr_eq ignores universe constraints. | Pierre-Marie Pédrot | |
| 2018-06-19 | Merge PR #7801: [vernac] Add option to force building really mutual ↵ | Enrico Tassi | |
| induction schemes | |||
| 2018-06-19 | Merge PR #7841: Remove Canary | Pierre-Marie Pédrot | |
| 2018-06-19 | [doc] Rewrite and document the prodn directive | Clément Pit-Claudel | |
| It was broken and undocumented. We dropped the git logs, too, so it wasn't clear who wrote it and why it was introduced in the first place. | |||
| 2018-06-19 | [doc] Fix a typo in the ssreflect chapter | Clément Pit-Claudel | |
| 2018-06-19 | [doc] Fix uncaught duplicate-label errors in the SSReflect chapter | Clément Pit-Claudel | |
| 2018-06-19 | [doc] Use productionlist instead of prodn in ring.rst | Clément Pit-Claudel | |
| 2018-06-19 | Merge PR #7714: Remove primitive-projection related data from the kernel | Maxime Dénès | |
| 2018-06-19 | Merge PR #7856: Fix #7829: Spurious documentation failures. | Maxime Dénès | |
| 2018-06-18 | Overlay for reference removal | Maxime Dénès | |
| 2018-06-18 | Merge PR #7855: Update section on adding your project to CI and link to ↵ | Emilio Jesus Gallego Arias | |
| example PR. | |||
| 2018-06-18 | Fix #7421: constr_eq ignores universe constraints. | Gaëtan Gilbert | |
| The test isn't quite the one in #7421 because that use of algebraic universes is wrong. | |||
| 2018-06-18 | Remove Canary. | whitequark | |
| This eliminates 3 uses of Obj from TCB. | |||
| 2018-06-18 | Fix #7829: Spurious documentation failures. | Théo Zimmermann | |
| We split a Require Import in two to avoid reaching the timeout. | |||
| 2018-06-18 | Merge PR #7840: Remove Hashcons.Hobj | Pierre-Marie Pédrot | |
| 2018-06-18 | Update section on adding your project to CI and link to example PR. | Théo Zimmermann | |
| 2018-06-18 | Remove reference name type. | Maxime Dénès | |
| reference was defined as Ident or Qualid, but the qualid type already permits empty paths. So we had effectively two representations for unqualified names, that were not seen as equal by eq_reference. We remove the reference type and replace its uses by qualid. | |||
| 2018-06-17 | Remove Hashcons.Hobj. | whitequark | |
| This eliminates 12 uses of Obj from TCB. | |||
| 2018-06-17 | Merge PR #7824: Fixes #7811 (uncaught Not_found in notation printer related ↵ | Pierre-Marie Pédrot | |
| to "match"). | |||
| 2018-06-17 | Merge PR #7848: Fix a typo in documentation | Théo Zimmermann | |
| 2018-06-17 | Merge PR #7822: cArray: proper invalid_arg exceptions | Pierre-Marie Pédrot | |
| 2018-06-17 | Merge PR #7844: Remove Elpi from Travis. | Emilio Jesus Gallego Arias | |
| 2018-06-17 | Merge PR #7828: [Spawn] no control sock on unix | Emilio Jesus Gallego Arias | |
| 2018-06-17 | Add introduction and credits to the TOC. | Théo Zimmermann | |
| Move credits to its own chapter (closes #6573). | |||
| 2018-06-17 | Move indexes on top on the TOC. Closes #7764. | Théo Zimmermann | |
| 2018-06-17 | Merge PR #7818: Do not allow spliting in res_pf, this is reserved for pretyping | Pierre-Marie Pédrot | |
| 2018-06-17 | Remove the proj_body field from the kernel. | Pierre-Marie Pédrot | |
| This was completely wrong, such a term could not even be type-checked by the kernel as it was internally using a match construct over a negative record. They were luckily only used in upper layers, namley printing and extraction. Recomputing the projection body might be costly in detyping, but this only happens when the compatibility flag is turned on, which is not the default. Such flag is probably bound to disappear anyways. Extraction should be fixed though so as to define directly primitive projections, similarly to what has been done in native compute. | |||
| 2018-06-17 | Remove the proj_eta field of the kernel. | Pierre-Marie Pédrot | |
| This field was not used inside the kernel and not used in performance-critical code where caching is essential, so we extrude the code that computes it out of the kernel. | |||
| 2018-06-17 | Remove special declaration of primitive projections in the kernel. | Pierre-Marie Pédrot | |
| This reduces kernel bloat and removes code from the TCB, as compatibility projections are now retypechecked as normal definitions would have been. This should have no effect on efficiency as this only happens once at definition time. | |||
| 2018-06-17 | Fixes #7811 (uncaught Not_found in notation printer related to "match"). | Hugo Herbelin | |
| 2018-06-17 | Getting rid of the const_proj field in the kernel. | Pierre-Marie Pédrot | |
| This field used to signal that a constant was the compatibility eta-expansion of a primitive projections, but since a previous cleanup in the kernel it had become useless. | |||
| 2018-06-17 | Merge PR #7749: [doc] Disable smartquotes conversion | Maxime Dénès | |
| 2018-06-17 | Merge PR #7752: [merge script] Check if the CI that was run is outdated. | Maxime Dénès | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |