| Commit message (Expand) | Author | Age | |
|---|---|---|---|
| * | 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 kerne... | Maxime Dénès | 2018-06-23 |
| |\ \ \ | |||
| * \ \ \ | 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 |
| | * | | | | | | Using more general information for primitive records. | Pierre-Marie Pédrot | 2018-06-23 |
| | * | | | | | | Change the proj_ind field from MutInd.t to inductive. | Pierre-Marie Pédrot | 2018-06-23 |
| |/ / / / / / | |||
| * | | | | | | 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 |
| |\ \ \ \ \ \ \ \ \ | |||
| | | | | | | * | | | | [ssr] document {}/view |  Enrico Tassi | 2018-06-22 |
| | | | | | | * | | | | [ssr] document rewrite {}foo | Enrico Tassi | 2018-06-22 |
| | | | | | | * | | | | [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 |
| | |_|_|_|_|/ / / / |/| | | | | | | | | |||
| | * | | | | | | | | [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 |
| |/ / / / / / / / | |||
| * | | | | | | | | 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 |
| * | | | | | | | | | | 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 understa... | Maxime Dénès | 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 fo... |  Pierre Courtieu | 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-21 |
| |/ / / / / / / / / / / / / | |||
| | | | * | | | | | | | | | | 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 direc... |  Emilio Jesus Gallego Arias | 2018-06-20 |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ | |||
| | | | | | | * | | | | | | | | Make Clément the secondary codeowner of doc/tools/coqrst. | Théo Zimmermann | 2018-06-20 |
| | |_|_|_|_|/ / / / / / / / |/| | | | | | | | | | | | | |||
| | * | | | | | | | | | | | | [coqtop] Give priority to stdlib load path over current directory | Maxime Dénès | 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 induction... | Enrico Tassi | 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 | 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-19 |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |||
| | | | | | | | * | | | | | | | | | | | 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 examp... | Emilio Jesus Gallego Arias | 2018-06-18 |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |||
| | | | | | | * | | | | | | | | | | | | | Fix #7421: constr_eq ignores universe constraints. | Gaëtan Gilbert | 2018-06-18 |
| | |_|_|_|_|/ / / / / / / / / / / / / |/| | | | | | | | | | | | | | | | | | |||
| | | | | * | | | | | | | | | | | | | | Remove Canary. | whitequark | 2018-06-18 |
 |
index : coq | |
| the Coq proof assistant |
| aboutsummaryrefslogtreecommitdiffhomepage |