| Commit message (Expand) | Author | Age | ||
|---|---|---|---|---|
| ... | ||||
| * | | | | | | | | | | | | | | | Merge PR #7851: Modernize the introduction of the reference manual. |  Maxime Dénès | 2018-06-26 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |_|_|_|_|_|_|_|_|/ / / / / / |/| | | | | | | | | | | | | | | ||||
| | | | | | * | | | | | | | | | | Activate the build of Ltac2 and Equations in the Windows installer. |  Théo Zimmermann | 2018-06-25 | |
| | | | | | * | | | | | | | | | | Reuse CI info to know which version of plugins to build on Windows. | Théo Zimmermann | 2018-06-25 | |
| * | | | | | | | | | | | | | | | Merge PR #7798: Remove hack skipping comparison of algebraic universes in sub... |  Matthieu Sozeau | 2018-06-25 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| | | | | | | | | | | * | | | | | | Clarify the message "this hint will only be used by eauto" |  Armaël Guéneau | 2018-06-25 | |
| | |_|_|_|_|_|_|_|_|/ / / / / / |/| | | | | | | | | | | | | | | ||||
| | | | | | | * | | | | | | | | | Fix for issue 7707: include Ltac2 and Equations in Windows build |  Michael Soegtrop | 2018-06-25 | |
| * | | | | | | | | | | | | | | | 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 | |
| | |_|_|/ / / / / / / / / / / |/| | | | | | | | | | | | | | ||||
| | | | | | | | | | | | | | * | Mini-update of version history with recent changes. |  Hugo Herbelin | 2018-06-25 | |
| | |_|_|_|_|_|_|_|_|_|_|_|/ |/| | | | | | | | | | | | | ||||
| | | | | | | | | | | * | | | Critical bugs: added #3243 and Gonthier's bug in lazy machine. | Hugo Herbelin | 2018-06-25 | |
| | |_|_|_|_|_|_|_|_|/ / / |/| | | | | | | | | | | | ||||
| * | | | | | | | | | | | | 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 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| | | | | | | | | | | | | | * | | | Documenting the syntax of mutual keywords. | Pierre-Marie Pédrot | 2018-06-24 | |
| | | | | | | | | | | | | | * | | | Added mention of mutual records to CHANGES. | Pierre-Marie Pédrot | 2018-06-24 | |
| | | | | | | | | | | | | | * | | | Adding various tests for mutual records. | Pierre-Marie Pédrot | 2018-06-24 | |
| | | | | | | | | | | | | | * | | | Handle mutual record at the vernac level. | Pierre-Marie Pédrot | 2018-06-24 | |
| | | | | | | | | | | | | | * | | | Handle mutual records in upper layers. | 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 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|/ / / / |/| | | | | | | | | | | | | | | | | | | | | | ||||
| | | | | | | | | | | | | | | | | | | | | * | | Fix #7704: get_toplevel_path needs normalised argv.(0) |  Gaëtan Gilbert | 2018-06-22 | |
| | | | | | | | | | | | | | | | | | | * | | | | Fix handling of universe context for expanded program obligations. |  Matthieu Sozeau | 2018-06-22 | |
| | |_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|/ / / / |/| | | | | | | | | | | | | | | | | | | | | ||||
| | | | | | | | | | | | | | | * | | | | | | | Remove hack skipping comparison of algebraic universes in subtyping. | Gaëtan Gilbert | 2018-06-22 | |
| | | | | | | | | | | | | | | * | | | | | | | Define and use UGraph.enforce_leq_alg for subtyping inference | Gaëtan Gilbert | 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 | |
| |/ / / / / / / / / / / / / / / / / / / | ||||
| | | | | | | | | | * / / / / / / / / / | Revert "Add a note about [ci skip] in CI README." | Théo Zimmermann | 2018-06-22 | |
| | |_|_|_|_|_|_|_|/ / / / / / / / / / |/| | | | | | | | | | | | | | | | | | ||||
| | | | | | | | | | | | | | | * | | | | Get rid of INSTALL.ide. List the dependency versions in INSTALL. | Théo Zimmermann | 2018-06-22 | |
| | | | | | | | | | | | | | | * | | | | Fix #7608: missing num package in INSTALL documentation. | Théo Zimmermann | 2018-06-22 | |
| | | | | | | | | | | | | | |/ / / / | ||||
| | | | | | | | | | | | | | * | | | | Fix Windows install script following removal of INSTALL.ide and move of INSTA... | Théo Zimmermann | 2018-06-22 | |
| | | | | | | | | | | | | | * | | | | Clarify further doc/README.md following Jim's comments. | Théo Zimmermann | 2018-06-22 | |
| | | | | | | | | | | | | | * | | | | Fix copyright dates in doc/LICENSE. | Théo Zimmermann | 2018-06-22 | |
| | | | | | | | | | | | | | * | | | | Improve doc/README.md. | Théo Zimmermann | 2018-06-22 | |
| | | | | | | | | | | | | | * | | | | Move INSTALL.doc into doc/README.md. | Théo Zimmermann | 2018-06-22 | |
| | |_|_|_|_|_|_|_|_|_|_|_|/ / / / |/| | | | | | | | | | | | | | | | ||||
 |
index : coq | |
| the Coq proof assistant |
| aboutsummaryrefslogtreecommitdiffhomepage |