| Commit message (Expand) | Author | Age | ||
|---|---|---|---|---|
| ... | ||||
| | | | | | | | | * | | [Sphinx] Move chapter 26 to new infrastructure |  Maxime Dénès | 2018-03-29 | |
| | | | | | | | |/ / | ||||
| | * | | | | | / / | Fix #6631: Derive Plugin gives "Anomaly: more than one statement". |  Pierre-Marie Pédrot | 2018-03-29 | |
| |/ / / / / / / / | ||||
| | | | | | | * | | [Sphinx] Add chapter 24 | Maxime Dénès | 2018-03-29 | |
| | | | | | | * | | [Sphinx] Move chapter 24 to new infrastructure | Maxime Dénès | 2018-03-29 | |
| | | | | | |/ / | ||||
| | | | | | * | | [Sphinx] Add chapter 23 | Maxime Dénès | 2018-03-29 | |
| | | | | | * | | [Sphinx] Move chapter 23 to new infrastructure | Maxime Dénès | 2018-03-29 | |
| | | | | |/ / | ||||
| | | | | * | | [Sphinx] Remove duplicate entry for command `Coercion` | Maxime Dénès | 2018-03-29 | |
| | | | | * | | [Sphinx] Add chapter 18 | Maxime Dénès | 2018-03-29 | |
| | | | | * | | [Sphinx] Move chapter 18 to new infrastructure | Maxime Dénès | 2018-03-29 | |
| | |_|_|/ / |/| | | | | ||||
| * | | | | | Merge PR #7057: Sphinx Chapter 20: Type Classes | Maxime Dénès | 2018-03-29 | |
| |\ \ \ \ \ | ||||
| * \ \ \ \ \ | Merge PR #7072: Update codeowners | Maxime Dénès | 2018-03-29 | |
| |\ \ \ \ \ \ | ||||
| | * | | | | | | Remove dev/doc/changes.md from files with a code owner. |  Théo Zimmermann | 2018-03-29 | |
| | | | | * | | | Supporting fix/cofix in Ltac pattern-matching (wish #7092). |  Hugo Herbelin | 2018-03-28 | |
| | | | | * | | | Patterns: Accepting patterns in PFix and PCofix and not only constr. | Hugo Herbelin | 2018-03-28 | |
| | | | | * | | | Adding Array.fold_left4. | Hugo Herbelin | 2018-03-28 | |
| | | | | * | | | Detyping: Adding a variant of share_names for patterns. | Hugo Herbelin | 2018-03-28 | |
| | | | | * | | | Detyping: Making detype_fix/detype_cofix polymorphic combinator (step 1). | Hugo Herbelin | 2018-03-28 | |
| | | | | * | | | Patternops: renaming an internal function to more closely match its effect. | Hugo Herbelin | 2018-03-28 | |
| | | | | * | | | Glob_ops: cosmetic renaming to reflect the type of objects. | Hugo Herbelin | 2018-03-28 | |
| * | | | | | | | Merge PR #7090: stm: don't propagate side effects when editing a proof |  Emilio Jesus Gallego Arias | 2018-03-28 | |
| |\ \ \ \ \ \ \ | ||||
| * \ \ \ \ \ \ \ | Merge PR #6961: [test-suite] Add backtracking test for `Load`. |  Enrico Tassi | 2018-03-28 | |
| |\ \ \ \ \ \ \ \ | ||||
| | | * | | | | | | | stm: don't propagate side effects when editing a proof | Enrico Tassi | 2018-03-27 | |
| | | | | | | | * | | Adding tacticals tclBINDFIRST/tclBINDLAST. | Hugo Herbelin | 2018-03-27 | |
| | | | | | | | * | | Export Proofview.undefined as "unsafe" primitive. | Hugo Herbelin | 2018-03-27 | |
| | | | | | | | * | | Adding informative variant of shelve_unifiable returning set of shelved evars. | Hugo Herbelin | 2018-03-27 | |
| | |_|_|_|_|_|/ / |/| | | | | | | | ||||
| * | | | | | | | | Merge PR #6835: Deprecate undocumented "intros until 0" in favor of "intros *" | Pierre-Marie Pédrot | 2018-03-27 | |
| |\ \ \ \ \ \ \ \ | ||||
| * \ \ \ \ \ \ \ \ | Merge PR #7062: Slightly refining some error messages about unresolvable evars. | Pierre-Marie Pédrot | 2018-03-27 | |
| |\ \ \ \ \ \ \ \ \ | ||||
| | | | | | | * | | | | [doc] Port Chapter 20 Type Classes to Sphinx |  Matthieu Sozeau | 2018-03-26 | |
| * | | | | | | | | | | Merge PR #6739: Tentative fix for #6520: camlcity.org unresponsive makes AppV... | Maxime Dénès | 2018-03-26 | |
| |\ \ \ \ \ \ \ \ \ \ | |_|_|_|/ / / / / / |/| | | | | | | | | | ||||
| | | | | | | * | | | | Move Classes.tex to type-classes.rst | Matthieu Sozeau | 2018-03-26 | |
| * | | | | | | | | | | Merge PR #6970: [vernac] Move `Quit` and `Drop` to the toplevel layer. | Enrico Tassi | 2018-03-26 | |
| |\ \ \ \ \ \ \ \ \ \ | |_|_|_|_|_|_|_|/ / |/| | | | | | | | | | ||||
| | | | | | | * | | | | Add Michael Soegtrop as a code owner for Windows build scripts. | Théo Zimmermann | 2018-03-26 | |
| | | | | | | * | | | | Use Pierre Corbineau GitHub nickname in CODEOWNERS. | Théo Zimmermann | 2018-03-26 | |
| | |_|_|_|_|/ / / / |/| | | | | | | | | ||||
| | | | * | | | | | | Slightly refining some error messages about unresolvable evars. | Hugo Herbelin | 2018-03-24 | |
| | |_|/ / / / / / |/| | | | | | | | ||||
| | | | * | | | | | Deprecate undocumented "intros until 0" in favor of "intros *". | Hugo Herbelin | 2018-03-23 | |
| | |_|/ / / / / |/| | | | | | | ||||
| * | | | | | | | Merge PR #7046: Switch maintainers for documentation | Théo Zimmermann | 2018-03-23 | |
| |\ \ \ \ \ \ \ | ||||
| * \ \ \ \ \ \ \ | Merge PR #7018: Fix typo in CHANGES. | Maxime Dénès | 2018-03-23 | |
| |\ \ \ \ \ \ \ \ | ||||
| * \ \ \ \ \ \ \ \ | Merge PR #7029: improve merge-pr script | Maxime Dénès | 2018-03-23 | |
| |\ \ \ \ \ \ \ \ \ | ||||
| | * | | | | | | | | | improve merge-pr script | Enrico Tassi | 2018-03-23 | |
| * | | | | | | | | | | Merge PR #7052: More precise wording about the merge process. | Théo Zimmermann | 2018-03-23 | |
| |\ \ \ \ \ \ \ \ \ \ | |_|_|_|_|_|_|/ / / |/| | | | | | | | | | ||||
| | * | | | | | | | | | More precise wording about the merge process. | Maxime Dénès | 2018-03-23 | |
| * | | | | | | | | | | Merge PR #7028: Fix #7026: ssr: applying an overloaded lemma as a view takes ... | Enrico Tassi | 2018-03-23 | |
| |\ \ \ \ \ \ \ \ \ \ | ||||
| * \ \ \ \ \ \ \ \ \ \ | Merge PR #6968: [stm] Never consider `Backtrack` as part of the script. | Enrico Tassi | 2018-03-23 | |
| |\ \ \ \ \ \ \ \ \ \ \ | ||||
| * \ \ \ \ \ \ \ \ \ \ \ | Merge PR #7025: Coq makefile: provide variables to extend the flags passed to... | Enrico Tassi | 2018-03-23 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ | ||||
| | * | | | | | | | | | | | | update CHANGES | Enrico Tassi | 2018-03-23 | |
| * | | | | | | | | | | | | | Merge PR #7030: [default.nix] Add dependencies of the merging script. |  Vincent Laporte | 2018-03-23 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| * \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #7031: Owners for developer tools | Théo Zimmermann | 2018-03-22 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ | |_|_|_|_|/ / / / / / / / / |/| | | | | | | | | | | | | | ||||
| | * | | | | | | | | | | | | | Owners for developer tools | Maxime Dénès | 2018-03-22 | |
| |/ / / / / / / / / / / / / | ||||
| * | | | | | | | | | | | | | Merge pull request #7040 from maximedenes/sphinx-doc-chapter-22 |  Guillaume Melquiond | 2018-03-22 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| | * \ \ \ \ \ \ \ \ \ \ \ \ | Merge branch 'master' into sphinx-doc-chapter-22 | Guillaume Melquiond | 2018-03-22 | |
| | |\ \ \ \ \ \ \ \ \ \ \ \ \ | |/ / / / / / / / / / / / / |/| | | | | | | | | | | | | | ||||
 |
index : coq | |
| the Coq proof assistant |
| aboutsummaryrefslogtreecommitdiffhomepage |