| Commit message (Expand) | Author | Age | ||
|---|---|---|---|---|
| ... | ||||
| | | | | | | | | | | | | | * | | [ssr] some fixes to the documentation markup |  Enrico Tassi | 2018-06-05 | |
| | | | | | | | | | | | | | * | | [sphinx] Start fixing SSR chapter. |  Théo Zimmermann | 2018-06-05 | |
| | |_|_|_|_|_|_|_|_|_|_|_|/ / |/| | | | | | | | | | | | | | ||||
| | | | | | * | | | | | | | | | More straightforward native compilation of primitive projections. |  Pierre-Marie Pédrot | 2018-06-05 | |
| | | | | | * | | | | | | | | | Use projection indices in native compilation rather than constant names. | Pierre-Marie Pédrot | 2018-06-05 | |
| | |_|_|_|/ / / / / / / / / |/| | | | | | | | | | | | | ||||
| * | | | | | | | | | | | | | Merge PR #7643: Fix #7631: native_compute fails to compile an example in Coq 8.8 | Pierre-Marie Pédrot | 2018-06-05 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| * \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #7690: Fixing typos in file Berardi.v | Pierre-Marie Pédrot | 2018-06-05 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ | |_|_|_|_|_|_|_|/ / / / / / |/| | | | | | | | | | | | | | ||||
| * | | | | | | | | | | | | | | Merge PR #7646: Fix #4714: Stack overflow with native compute | Pierre-Marie Pédrot | 2018-06-05 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| * \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #7099: Stronger invariants in unification signature. |  Matthieu Sozeau | 2018-06-05 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| * \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #7453: Refuse to parse empty [Context] command. | Matthieu Sozeau | 2018-06-05 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| * \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #7495: Fix restrict_universe_context | Matthieu Sozeau | 2018-06-05 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |_|_|_|_|_|_|_|_|_|/ / / / / / / |/| | | | | | | | | | | | | | | | | ||||
| | | | | | | | | | | * | | | | | | | Make direct invocations of `simple apply` obey `Opaque` directive. |  Maxime Dénès | 2018-06-05 | |
| | |_|_|_|_|_|_|_|_|/ / / / / / / |/| | | | | | | | | | | | | | | | ||||
| | | | | | | * | | | | | | | | | | 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 | |
 |
index : coq | |
| the Coq proof assistant |
| aboutsummaryrefslogtreecommitdiffhomepage |