aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2018-03-02CHANGES entry for #6791.Théo Zimmermann
2018-03-02Remove 8.5 compatibility support.Théo Zimmermann
2018-03-02Remove VOld compatibility flag.Théo Zimmermann
2018-03-02Turn warning for deprecated notations on.Théo Zimmermann
Fix new deprecation warnings in the standard library.
2018-03-02Remove the deprecation for some 8.2-8.5 compatibility aliases.Théo Zimmermann
This was decided during the Fall WG (2017). The aliases that are kept as deprecated are the ones where the difference is only a prefix becoming a qualified module name. The intention is to turn the warning for deprecated notations on. We change the compat version to 8.6 to allow the removal of VOld and V8_5.
2018-03-01Merge PR #6856: travis: elpi needs findlib >= 1.5Maxime Dénès
2018-03-01Merge PR #6864: Remove empty, wrongly located, doc file.Maxime Dénès
2018-03-01Merge PR #6861: Typo in the documentation of the `pattern` tacticMaxime Dénès
2018-03-01Merge PR #6850: Fix #6751 trust_file_cache logic was invertedMaxime Dénès
2018-02-28travis: elpi needs findlib >= 1.5Enrico Tassi
2018-02-28tavis: make the . in pkg.version part of $VERSIONEnrico Tassi
2018-02-28Merge PR #6847: Fix make source-docMaxime Dénès
2018-02-28Merge PR #6854: comment "resolvability" bit in Evd.evar_mapMaxime Dénès
2018-02-28Merge PR #6852: [stdlib] move “Require” out of sectionsMaxime Dénès
2018-02-28Merge PR #6853: Add a comment on EConstr.to_constr regarding evar-freeness.Maxime Dénès
2018-02-28Merge PR #1026: changed statements of Rpower_lt and Rle_power and added lemmasMaxime Dénès
2018-02-28Merge PR #6756: Fix issue with spurious timing test failuresMaxime Dénès
2018-02-28Merge PR #6788: Fixes #6787 (minus sign interpreted by coqdoc as a bullet in ↵Maxime Dénès
Ring_theory.v)
2018-02-28Merge PR #6789: Check whitespace errors per-commit.Maxime Dénès
2018-02-28Merge PR #6734: dest_{prod,lam}: no Cast case (it's removed by whd)Maxime Dénès
2018-02-28Merge PR #6823: Fixes #6821 (bug in protecting notation printing from ↵Maxime Dénès
infinite eta-expansion)
2018-02-28Merge PR #6812: Rename release_lexer_state to the more descriptive ↵Maxime Dénès
get_lexer_state.
2018-02-28Merge PR #6752: Remove from CircleCI builds that are already taken care of ↵Maxime Dénès
by Travis.
2018-02-28Remove empty, wrongly located, doc file.Théo Zimmermann
2018-02-27Typo in the documentation of the `pattern` tacticJoachim Breitner
2018-02-27comment "resolvability" bit in Evd.evar_mapEnrico Tassi
2018-02-27Fix #6751 trust_file_cache logic was invertedGaëtan Gilbert
Bug introduced by 675a1dc401eb9a5540ba5bc9a522c1f84d4c3d54
2018-02-27Add a comment on EConstr.to_constr regarding evar-freeness.Pierre-Marie Pédrot
2018-02-27[stdlib] move “Require” out of sectionsVincent Laporte
2018-02-27Use relative path for show_latex_messagesmrmr1993
2018-02-27Use MYCAMLP5LIB instead of undefined MYCAMLP4LIBmrmr1993
This completes the work of b60906cc3ee3f994babf9cceff2971bd03485f2f
2018-02-24[test-suite] Move sed scripts into bash arraysJason Gross
As per https://github.com/coq/coq/pull/6756/files#r168028764
2018-02-24Merge PR #6543: Update headers and creditsMaxime Dénès
2018-02-24Merge PR #6784: New IR in VM: ClambdaMaxime Dénès
2018-02-24Merge PR #6819: Document Arguments extra scopes flagMaxime Dénès
2018-02-24Merge PR #6776: Fixes bug #6774 (anomaly with ill-typed template polymorphism).Maxime Dénès
2018-02-24Merge PR #6803: coqdev.el: add space at the end of compile-commandMaxime Dénès
2018-02-24Merge PR #6599: Decimals in preludeMaxime Dénès
2018-02-24Merge PR #6745: [ast] Improve precision of Ast location recognition in ↵Maxime Dénès
serialization.
2018-02-23Check whitespace errors per-commit.Gaëtan Gilbert
Otherwise it is possible to detect errors that are not fixed by git rebase since that works per-commit.
2018-02-23New IR in VM: Clambda.Maxime Dénès
This intermediate representation serves two purposes: 1- It is a preliminary step for primitive machine integers, as iterators will be compiled to Clambda. 2- It makes the VM compilation passes closer to the ones of native_compute. Once we unifiy the representation of values, we should be able to factorize the lambda-code generation between the two compilers, as well as the reification code. This code was written by Benjamin Grégoire and myself.
2018-02-23Fix map iterator on nativelambda.Maxime Dénès
2018-02-23Fixes #6821 (bug in protecting notation printing from infinite eta-expansion).Hugo Herbelin
More precisely when matching "f t" with "(fun ?x => .. ((fun ?x' => ?y) ?z') ..) ?z" do not allow expansion of f since otherwise, we recursively have to match "f t" with the same pattern.
2018-02-22Document Arguments extra scopes flagJasper Hugunin
2018-02-22Tweak developer documentation.Jim Fehrle
2018-02-22Rename 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
We follow the suggestions in #402 and turn uses of `Loc.located` in `vernac` into `CAst.t`. The impact should be low as this change mostly affects top-level vernaculars. With this change, we are even closer to automatically map a text document to its AST in a programmatic way.
2018-02-21Remove from CircleCI builds that are already taken care of by Travis.Théo Zimmermann
2018-02-21Merge PR #6604: Extend `zify_N` with knowledge about `N.pred`Maxime Dénès
2018-02-21Merge PR #6282: proposed fix for issue #3213: extra variable m in Lt.S_predMaxime Dénès
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-28 13:12:25 +0000