| Commit message (Expand) | Author | Age | ||
|---|---|---|---|---|
| ... | ||||
| | | | | | | * | | | | | | | | | Fix #7631: native_compute fails to compile an example in Coq 8.8 |  Maxime Dénès | 2018-06-04 | |
| | |_|_|_|_|/ / / / / / / / / |/| | | | | | | | | | | | | | ||||
| * | | | | | | | | | | | | | | Merge PR #7315: An attempt to clarify error message for Arguments needing "re... | Maxime Dénès | 2018-06-04 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| | | | | | | | | | * | | | | | | Tests for part of #7068 and for #7076 (vm/native_compute and return predicate). |  Hugo Herbelin | 2018-06-04 | |
| | | | | | | | | | * | | | | | | Preserving "canonical" form of return predicate in native_compute. | Hugo Herbelin | 2018-06-04 | |
| | | | | | | | | | * | | | | | | Preserving "canonical" form of return predicate in vm_compute. | Hugo Herbelin | 2018-06-04 | |
| | |_|_|_|_|_|_|_|/ / / / / / |/| | | | | | | | | | | | | | ||||
| * | | | | | | | | | | | | | | Merge PR #7229: Deprecate implicit tactic solving. | Hugo Herbelin | 2018-06-04 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| * \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #7486: Update old parts of CHANGES to use current bug numbers. | Hugo Herbelin | 2018-06-04 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| * \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #7481: document 7025 (coq_makefile flag variables) | Maxime Dénès | 2018-06-04 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| * \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #7596: [ci] [windows] Use newer OCaml version. |  Michael Soegtrop | 2018-06-04 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| * \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #7655: Refactor parsing rules for Hint Resolve -> and Hint Resolve <- |  Pierre-Marie Pédrot | 2018-06-04 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| | | | | | | | | | | | | | | * | | | | | [econstr] Remove some Unsafe.to_constr use. |  Emilio Jesus Gallego Arias | 2018-06-04 | |
| | | | | | | | | | | | | | | * | | | | | [termops] Update type of function, anyways not used in the codebase. | Emilio Jesus Gallego Arias | 2018-06-04 | |
| | | | | | | | | | | | | | | * | | | | | [vernac] Switch back `auto_ind_decl` to Constr. | Emilio Jesus Gallego Arias | 2018-06-04 | |
| | |_|_|_|_|_|_|_|_|_|_|_|_|/ / / / / |/| | | | | | | | | | | | | | | | | | ||||
| | | | | | | | | | | | | * | | | | | | Make whitespace linter not check for trailing newlines. |  Gaëtan Gilbert | 2018-06-04 | |
| * | | | | | | | | | | | | | | | | | | Merge PR #7601: Fix notation for code snippet in documentation | Maxime Dénès | 2018-06-04 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| * \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #7418: Actually take advantage of the normalization status of kernel... | Maxime Dénès | 2018-06-04 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |_|_|_|_|_|_|_|_|_|_|_|_|/ / / / / / |/| | | | | | | | | | | | | | | | | | | ||||
| | | | | | | | | | | | | | | * | | | | | test suite: make target to regenerate failing output tests | Gaëtan Gilbert | 2018-06-04 | |
| * | | | | | | | | | | | | | | | | | | | Merge PR #7199: Fixes #7195: missing freshness condition in Ltac pattern-matc... |  Matthieu Sozeau | 2018-06-04 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| * \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #7112: Fix #6770: fixpoint loses locality info in proof mode. | Matthieu Sozeau | 2018-06-04 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| * \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #7114: Fix #7113: Program Let Fixpoint in section causes anomaly | Matthieu Sozeau | 2018-06-04 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| * \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #7189: Fix #5539: algebraic universe produced by cases. | Matthieu Sozeau | 2018-06-04 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| * \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #7349: Fix an anomaly when calling Obligation 0 or Obligation -1. | Matthieu Sozeau | 2018-06-04 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| | | | | | | | | | | | | | | | | * | | | | | | | | Documenting the API change. | Pierre-Marie Pédrot | 2018-06-04 | |
| | | | | | | | | | | | | | | | | * | | | | | | | | Adding an overlay for the Equations plugin. | Pierre-Marie Pédrot | 2018-06-04 | |
| | | | | | | | | | | | | | | | | * | | | | | | | | Stronger invariants in unification signature. | Pierre-Marie Pédrot | 2018-06-04 | |
| | |_|_|_|_|_|_|_|_|_|_|_|_|_|_|/ / / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | ||||
| * | | | | | | | | | | | | | | | | | | | | | | | Merge PR #7013: Fixes #7011: Fix/CoFix were not considered in main loop of ta... | Matthieu Sozeau | 2018-06-04 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| * \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #7216: Replace uses of Termops.dependent by more specific functions. | Matthieu Sozeau | 2018-06-04 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| * \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #7552: Fix #7539: Checker does not properly handle negative coinduct... | Matthieu Sozeau | 2018-06-04 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| * \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #7590: Fix #7586: Anomaly "Uncaught exception Not_found". | Matthieu Sozeau | 2018-06-04 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|/ / |/| | | | | | | | | | | | | | | | | | | | | | | | | | ||||
| | | | | | | | | | | | | | | | | * | | | | | | | | | | Documenting the deprecation. | Pierre-Marie Pédrot | 2018-06-04 | |
| | | | | | | | | | | | | | | | | * | | | | | | | | | | Deprecate implicit tactic solving. | Pierre-Marie Pédrot | 2018-06-04 | |
| | |_|_|_|_|_|_|_|_|_|_|_|_|_|_|/ / / / / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | ||||
| * | | | | | | | | | | | | | | | | | | | | | | | | | Merge PR #7249: Cleaning, documentation, uniformisation of the Coq extension ... | Pierre-Marie Pédrot | 2018-06-04 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| * \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #7619: Mention test-suite in PR template | Maxime Dénès | 2018-06-04 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| * \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #7648: Indicate in the doc that clearbody can take several idents | Maxime Dénès | 2018-06-04 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| * \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #7496: Fix #4403: insufficient handling of type-in-type in kernel. | Maxime Dénès | 2018-06-04 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| * \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #7657: Fix a couple typos in deprecation messages | Pierre-Marie Pédrot | 2018-06-04 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| * \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #7640: Small refactoring to clarify make_local_hint_db. | Pierre-Marie Pédrot | 2018-06-04 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| * \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #7649: Remove some dead code in class_tactics.ml | Pierre-Marie Pédrot | 2018-06-04 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | * | Statment -> Statement | Hugo Herbelin | 2018-06-03 | |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | * | | | | | Fixing typos in file Berardi.v | Hugo Herbelin | 2018-06-03 | |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | |_|_|/ | | | | | | | | | | | | | | | | | | | | | | | | | | | |/| | | | ||||
| * | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Merge PR #7682: Fixes #7641: more detailed message about disjunctive patterns... | Emilio Jesus Gallego Arias | 2018-06-03 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| * \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #7689: configure: fix warning printing | Emilio Jesus Gallego Arias | 2018-06-03 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| * \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #7637: Fix an outdated comment refering to lib/dnet.mli | Pierre-Marie Pédrot | 2018-06-03 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| | | * | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | configure: fix warning printing | Gaëtan Gilbert | 2018-06-03 | |
| | |/ / / / / / / / / / / / / / / / / / / / / / / / / / / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | ||||
| | | | | | | | | | * | | | | | | | | | | | | | | | | | | | | | | | | Further sharing in CList. | Hugo Herbelin | 2018-06-03 | |
| | | | | | | | | | * | | | | | | | | | | | | | | | | | | | | | | | | Cleaning, documentation, uniformisation of the Coq extension of List. | Hugo Herbelin | 2018-06-03 | |
| | |_|_|_|_|_|_|_|/ / / / / / / / / / / / / / / / / / / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | ||||
| * | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Merge PR #7683: [lib] Fix wrong deprecation annotations. | Pierre-Marie Pédrot | 2018-06-03 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|/ / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | ||||
| | | | * | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Fixes #7641: more detailed message for disjunctive patterns with different vars. | Hugo Herbelin | 2018-06-03 | |
| * | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Merge PR #7656: CI for QuickChick and ext-lib | Emilio Jesus Gallego Arias | 2018-06-03 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| | * | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Update .gitlab to use newer ocaml |  Leonidas Lampropoulos | 2018-06-02 | |
 |
index : coq | |
| the Coq proof assistant |
| aboutsummaryrefslogtreecommitdiffhomepage |