| Commit message (Collapse) | Author | Age | |
|---|---|---|---|
| * | Merge PR #7919: Fix equality check on global names from native compute. |  Maxime Dénès | 2018-06-26 |
| |\ | |||
| * \ | Merge PR #7851: Modernize the introduction of the reference manual. | Maxime Dénès | 2018-06-26 |
| |\ \ | |||
| * \ \ | Merge PR #7798: Remove hack skipping comparison of algebraic universes in ↵ |  Matthieu Sozeau | 2018-06-25 |
| |\ \ \ | | | | | | | | | | | | | subtyping. | ||
| * \ \ \ | Merge PR #7559: Existing Class noop when already a class + warning. | Matthieu Sozeau | 2018-06-25 |
| |\ \ \ \ | |||
| | | | | * | Fix equality check on global names from native compute. |  Pierre-Marie Pédrot | 2018-06-25 |
| | |_|_|/ |/| | | | | | | | | | | | | | | | | | | | Not sure it could have led to a soundness bug, but this is definitely serious enough to deserve a backport. Also made the code robust by listing all the constructors. | ||
| * | | | | Merge PR #7620: [ssr] rewrite: turn anomaly into regular error | Maxime Dénès | 2018-06-25 |
| |\ \ \ \ | |||
| * \ \ \ \ | Merge PR #7895: Revert "Add a note about [ci skip] in CI README." |  Emilio Jesus Gallego Arias | 2018-06-24 |
| |\ \ \ \ \ | |||
| * \ \ \ \ \ | Merge PR #7805: Towards listing the critical bugs of the history of Coq. |  Théo Zimmermann | 2018-06-24 |
| |\ \ \ \ \ \ | |||
| * \ \ \ \ \ \ | Merge PR #7772: [native_compute] Delay computations with toplevel match | Pierre-Marie Pédrot | 2018-06-24 |
| |\ \ \ \ \ \ \ | |||
| * \ \ \ \ \ \ \ | Merge PR #7784: Remove Tutorials from a few other places following #7466. | Maxime Dénès | 2018-06-24 |
| |\ \ \ \ \ \ \ \ | |||
| * \ \ \ \ \ \ \ \ | Merge PR #7614: Simplify the code that handles trust of side-effects in ↵ | Maxime Dénès | 2018-06-23 |
| |\ \ \ \ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | kernel typing. | ||
| * \ \ \ \ \ \ \ \ \ | Merge PR #7236: [ssr] simpler semantics for delayed clears | Maxime Dénès | 2018-06-23 |
| |\ \ \ \ \ \ \ \ \ \ | |||
| * \ \ \ \ \ \ \ \ \ \ | Merge PR #7827: [engine] safe [add_unification_pb] interface | Pierre-Marie Pédrot | 2018-06-23 |
| |\ \ \ \ \ \ \ \ \ \ \ | |||
| * \ \ \ \ \ \ \ \ \ \ \ | Merge PR #7750: Handle mutual records in the kernel | Maxime Dénès | 2018-06-23 |
| |\ \ \ \ \ \ \ \ \ \ \ \ | |||
| | * | | | | | | | | | | | | Adapt the kernel to generate proper data for mutual records. | Pierre-Marie Pédrot | 2018-06-23 |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Upper layers are still not able to handle mutual records though. | ||
| | * | | | | | | | | | | | | Using more general information for primitive records. | Pierre-Marie Pédrot | 2018-06-23 |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This brings more compatibility with handling of mutual primitive records in the kernel. | ||
| | * | | | | | | | | | | | | Change the proj_ind field from MutInd.t to inductive. | Pierre-Marie Pédrot | 2018-06-23 |
| |/ / / / / / / / / / / / | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This is a first step towards the acceptance of mutual record types in the kernel. | ||
| * | | | | | | | | | | | | Merge PR #7715: Simplify the cooking of primitive projections. | Maxime Dénès | 2018-06-23 |
| |\ \ \ \ \ \ \ \ \ \ \ \ | |||
| * \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #7600: Faster and cleaner fconstr-to-constr conversion function. | Maxime Dénès | 2018-06-22 |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ | |||
| * \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #7893: Update dpdgraph branch name | Théo Zimmermann | 2018-06-22 |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ | |||
| * \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #7776: [ssr] Fix rewrite with universes | Maxime Dénès | 2018-06-22 |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |||
| | | | | | | | | | | | | | | * | | Remove hack skipping comparison of algebraic universes in subtyping. |  Gaëtan Gilbert | 2018-06-22 |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | When inferring [u <= v+k] I replaced the exception and instead add [u <= v]. This is trivially sound and it doesn't seem possible to have the one without the other (except specially for [Set <= v+k] which was already handled). I don't know an example where this used to fail and now succeeds (the point was to remove an anomaly, but the example ~~~ Module Type SG. Definition DG := Type. End SG. Module MG : SG. Definition DG := Type : Type. Fail End MG. ~~~ now fails with universe inconsistency. Fix #7695 (soundness bug!). | ||
| | | | | | | | | | | | | | | * | | Define and use UGraph.enforce_leq_alg for subtyping inference | Gaëtan Gilbert | 2018-06-22 |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Not sure if worth using in other places. | ||
| | | | | | | * | | | | | | | | | | [ssr] document {}/view |  Enrico Tassi | 2018-06-22 |
| | | | | | | | | | | | | | | | | | |||
| | | | | | | * | | | | | | | | | | [ssr] document rewrite {}foo | Enrico Tassi | 2018-06-22 |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | It was used in some examples, but never fully documented | ||
| | | | | | | * | | | | | | | | | | [ssr] implement {}/v as a short hand for {v}/v when v is an id | Enrico Tassi | 2018-06-22 |
| | | | | | | | | | | | | | | | | | |||
| | | | | | | * | | | | | | | | | | [ssr] simplify delayed clears | Enrico Tassi | 2018-06-22 |
| | |_|_|_|_|/ / / / / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | - we always rename - we compile {clear}/view to /view{clear} | ||
| | * | | | | | | | | | | | | | | [ssr] test case for rewrite and set on univ poly keys | Enrico Tassi | 2018-06-22 |
| | | | | | | | | | | | | | | | | |||
| | * | | | | | | | | | | | | | | [ssr] matching: use eq_constr_nounivs in approximated matching | Enrico Tassi | 2018-06-22 |
| | | | | | | | | | | | | | | | | |||
| | * | | | | | | | | | | | | | | [ssr] set: merge universe constraints before type checking the term | Enrico Tassi | 2018-06-22 |
| |/ / / / / / / / / / / / / / | |||
| | | | | | | | | | * / / / / | Revert "Add a note about [ci skip] in CI README." | Théo Zimmermann | 2018-06-22 |
| | |_|_|_|_|_|_|_|/ / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This reverts commit 3a44a190a7f5d057b6a4bcb50124b42d83f3d03d. | ||
| * | | | | | | | | | | | | | 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 |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ | |||
| | | | * | | | | | | | | | | | | Update dpdgraph branch name | Gaëtan Gilbert | 2018-06-21 |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | See https://github.com/Karmaki/coq-dpdgraph/issues/50 for context | ||
| * | | | | | | | | | | | | | | | 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 | 2018-06-21 |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | understands. | ||
| * \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #7865: Fix #7432: Grammar token @term points to the SSR chapter. | Maxime Dénès | 2018-06-21 |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |||
| | | | | | | | | | | | | | | | * | | Remove enforce_leq from checker | Gaëtan Gilbert | 2018-06-21 |
| | | | | | | | | | | | | | | | | | | |||
| * | | | | | | | | | | | | | | | | | Merge PR #7842: Fix #7836: tools/inferior-coq.el uses next-line instead of ↵ |  Pierre Courtieu | 2018-06-21 |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | forward-line. | ||
| * \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | 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-21 |
| |/ / / / / / / / / / / / / / / / / / | |||
| | | | | | | | | | | | | | | | | | * | Mention Company-Coq as well. | Théo Zimmermann | 2018-06-20 |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We put it in a footnote otherwise the sentence was starting to be really long. Footnotes need to be in index.rst to really appear at the bottom of the index page. | ||
| | | | | | | | | | | | | | | | | | * | Add a good reference for Proof-General as suggested by Clément. | Théo Zimmermann | 2018-06-20 |
| | | | | | | | | | | | | | | | | | | | |||
| | | | | | | | | | | | | | | | | | * | Modernize the introduction of the reference manual. | Théo Zimmermann | 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 | 2018-06-20 |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | directory | ||
| | | | | | | | | | | | | | | | * | | | [ssr] test case for rewrite (setoid) making the goal illtyped | Enrico Tassi | 2018-06-20 |
| | | | | | | | | | | | | | | | | | | | |||
| | | | | | | | | | | | | | | | * | | | [ssr] rewrite: turn anomaly into regular error | Enrico Tassi | 2018-06-20 |
| | |_|_|_|_|_|_|_|_|_|_|_|_|_|/ / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | I think the bug was introduces when apply_type was made safe. In the test joint to #7255 rewrite (setoid case) generates an ill-typed goal and apply_type raises a Pretype_error. It is unclear to me why the tactic monad does not turn the pretype_error into a UserError | ||
 |
index : coq | |
| the Coq proof assistant |
| aboutsummaryrefslogtreecommitdiffhomepage |