Commit message (Expand) | Author | Age | ||
---|---|---|---|---|
... | ||||
| | * | | | | | | | | | Fixing rewriting in side conditions for "rewrite in *" and "rewrite in * |-". | Hugo Herbelin | 2018-03-01 | |
| | | |_|/ / / / / / | | |/| | | | | | | | ||||
| | | | | * | | | | | Moving code for "simple induction"/"simple destruct" to coretactics.ml4. | Hugo Herbelin | 2018-03-01 | |
* | | | | | | | | | | Merge PR #6856: travis: elpi needs findlib >= 1.5 | Maxime Dénès | 2018-03-01 | |
|\ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ | Merge PR #6864: Remove empty, wrongly located, doc file. | Maxime Dénès | 2018-03-01 | |
|\ \ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6861: Typo in the documentation of the `pattern` tactic | Maxime Dénès | 2018-03-01 | |
|\ \ \ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6850: Fix #6751 trust_file_cache logic was inverted | Maxime Dénès | 2018-03-01 | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| | | | | | | | * | | | | | | [toplevel] Update state when `Drop` exception is thrown [#6872] | Emilio Jesus Gallego Arias | 2018-02-28 | |
| | | | | | | |/ / / / / / | | | | | | |/| | | | | | | ||||
| | | | | | | | | | * | | | [toplevel] Move beautify to its own pass. | Emilio Jesus Gallego Arias | 2018-02-28 | |
| | | | | | |_|_|_|/ / / | | | | | |/| | | | | | | ||||
| | | | | * | | | | | | | [test-suite] Add a basic test-case for `Load`. | Emilio Jesus Gallego Arias | 2018-02-28 | |
| | | | | * | | | | | | | [toplevel] [vernac] Remove Load hack and check supported scenarios. | Emilio Jesus Gallego Arias | 2018-02-28 | |
| | | | | |/ / / / / / | ||||
| | | | | | | | * / / | [econstr] Continue consolidation of EConstr API under `interp`. | Emilio Jesus Gallego Arias | 2018-02-28 | |
| | | | | | |_|/ / / | | | | | |/| | | | | ||||
| | | | * | | | | | | travis: elpi needs findlib >= 1.5 | Enrico Tassi | 2018-02-28 | |
| | | | * | | | | | | tavis: make the . in pkg.version part of $VERSION | Enrico Tassi | 2018-02-28 | |
* | | | | | | | | | | Merge PR #6847: Fix make source-doc | Maxime Dénès | 2018-02-28 | |
|\ \ \ \ \ \ \ \ \ \ | |_|_|_|_|/ / / / / |/| | | | | | | | | | ||||
* | | | | | | | | | | Merge PR #6854: comment "resolvability" bit in Evd.evar_map | Maxime Dénès | 2018-02-28 | |
|\ \ \ \ \ \ \ \ \ \ | |_|_|_|_|_|_|/ / / |/| | | | | | | | | | ||||
* | | | | | | | | | | Merge PR #6852: [stdlib] move “Require” out of sections | Maxime Dénès | 2018-02-28 | |
|\ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ | Merge PR #6853: Add a comment on EConstr.to_constr regarding evar-freeness. | Maxime Dénès | 2018-02-28 | |
|\ \ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ \ | Merge PR #1026: changed statements of Rpower_lt and Rle_power and added lemmas | Maxime Dénès | 2018-02-28 | |
|\ \ \ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6756: Fix issue with spurious timing test failures | Maxime Dénès | 2018-02-28 | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6788: Fixes #6787 (minus sign interpreted by coqdoc as a bullet in ... | Maxime Dénès | 2018-02-28 | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6789: Check whitespace errors per-commit. | Maxime Dénès | 2018-02-28 | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6734: dest_{prod,lam}: no Cast case (it's removed by whd) | Maxime Dénès | 2018-02-28 | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6823: Fixes #6821 (bug in protecting notation printing from infinit... | Maxime Dénès | 2018-02-28 | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6812: Rename release_lexer_state to the more descriptive get_lexer_... | Maxime Dénès | 2018-02-28 | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6752: Remove from CircleCI builds that are already taken care of by... | Maxime Dénès | 2018-02-28 | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |_|_|_|_|_|_|_|_|_|_|_|_|_|_|/ / / / |/| | | | | | | | | | | | | | | | | | | ||||
| | | | | | | | | | | | | | | * | | | | Remove empty, wrongly located, doc file. | Théo Zimmermann | 2018-02-28 | |
| |_|_|_|_|_|_|_|_|_|_|_|_|_|/ / / / |/| | | | | | | | | | | | | | | | | | ||||
| | | | | | | | | | | | | | * | | | | Typo in the documentation of the `pattern` tactic | Joachim Breitner | 2018-02-27 | |
| |_|_|_|_|_|_|_|_|_|_|_|_|/ / / / |/| | | | | | | | | | | | | | | | | ||||
| | | | | | | | | | | * | | | | | | comment "resolvability" bit in Evd.evar_map | Enrico Tassi | 2018-02-27 | |
| |_|_|_|_|_|_|_|_|_|/ / / / / / |/| | | | | | | | | | | | | | | | ||||
| | | | | | | | | | | | | | * | | Update headers following #6543. | Théo Zimmermann | 2018-02-27 | |
| |_|_|_|_|_|_|_|_|_|_|_|_|/ / |/| | | | | | | | | | | | | | | ||||
| | | | | | | | | | | | * | | | Fix #6751 trust_file_cache logic was inverted | Gaëtan Gilbert | 2018-02-27 | |
| |_|_|_|_|_|_|_|_|_|_|/ / / |/| | | | | | | | | | | | | | ||||
| | | | | | | | | * | | | | | Add a comment on EConstr.to_constr regarding evar-freeness. | Pierre-Marie Pédrot | 2018-02-27 | |
| |_|_|_|_|_|_|_|/ / / / / |/| | | | | | | | | | | | | ||||
| | | | | | | | | * | | | | [stdlib] move “Require” out of sections | Vincent Laporte | 2018-02-27 | |
| |_|_|_|_|_|_|_|/ / / / |/| | | | | | | | | | | | ||||
| | | | | | | | | * | | | Use relative path for show_latex_messages | mrmr1993 | 2018-02-27 | |
| | | | | | | | | * | | | Use MYCAMLP5LIB instead of undefined MYCAMLP4LIB | mrmr1993 | 2018-02-27 | |
| |_|_|_|_|_|_|_|/ / / |/| | | | | | | | | | | ||||
| | | | | | | * | | | | [test-suite] Move sed scripts into bash arrays | Jason Gross | 2018-02-24 | |
* | | | | | | | | | | | Merge PR #6543: Update headers and credits | Maxime Dénès | 2018-02-24 | |
|\ \ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6784: New IR in VM: Clambda | Maxime Dénès | 2018-02-24 | |
|\ \ \ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6819: Document Arguments extra scopes flag | Maxime Dénès | 2018-02-24 | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6776: Fixes bug #6774 (anomaly with ill-typed template polymorphism). | Maxime Dénès | 2018-02-24 | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6803: coqdev.el: add space at the end of compile-command | Maxime Dénès | 2018-02-24 | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6599: Decimals in prelude | Maxime Dénès | 2018-02-24 | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6745: [ast] Improve precision of Ast location recognition in serial... | Maxime Dénès | 2018-02-24 | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| | | | | | | | | | | | * | | | | | | Check whitespace errors per-commit. | Gaëtan Gilbert | 2018-02-23 | |
| | | | | | * | | | | | | | | | | | | New IR in VM: Clambda. | Maxime Dénès | 2018-02-23 | |
| | | | | | * | | | | | | | | | | | | Fix map iterator on nativelambda. | Maxime Dénès | 2018-02-23 | |
| | | | | | | |_|_|_|_|/ / / / / / | | | | | | |/| | | | | | | | | | | ||||
| | | | | | | | | | * | | | | | | | Fixes #6821 (bug in protecting notation printing from infinite eta-expansion). | Hugo Herbelin | 2018-02-23 | |
| |_|_|_|_|_|_|_|_|/ / / / / / / |/| | | | | | | | | | | | | | | | ||||
| | | | | * | | | | | | | | | | | Document Arguments extra scopes flag | Jasper Hugunin | 2018-02-22 | |
| |_|_|_|/ / / / / / / / / / / |/| | | | | | | | | | | | | | | ||||
| | | | | | | | * | | | | | | | Tweak developer documentation. | Jim Fehrle | 2018-02-22 | |
| | | | | | | | * | | | | | | | Rename release_lexer_state to the more descriptive get_lexer_state. | Jim Fehrle | 2018-02-22 | |
| | | | | | |_|/ / / / / / / | | | | | |/| | | | | | | | | ||||
| * | | | / | | | | | | | | | [ast] Improve precision of Ast location recognition in serialization. | Emilio Jesus Gallego Arias | 2018-02-22 | |
|/ / / / / / / / / / / / / |