aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2018-03-04Merge PR #6736: [toplevel] Move beautify to its own pass.Maxime Dénès
2018-03-04Merge PR #6511: [econstr] Continue consolidation of EConstr API under `interp`.Maxime Dénès
2018-03-04Merge PR #6876: Unify Const_sorts and Const_type, and remove VsortMaxime Dénès
2018-03-04Merge PR #6846: Moving code for "simple induction"/"simple destruct" to ↵Maxime Dénès
coretactics.ml4.
2018-03-04Merge PR #6885: [stm] Partial fix for bug #6884 [location missing from ↵Maxime Dénès
replay nodes]
2018-03-04Merge PR #6873: [toplevel] Update state when `Drop` exception is thrown [#6872]Maxime Dénès
2018-03-04Merge PR #6882: Harden gitattributes against core.whitespace configuration.Maxime Dénès
2018-03-04Merge PR #6879: Fix #6878: univ undefined for [with Definition] bad instance ↵Maxime Dénès
size.
2018-03-04Merge PR #6676: [proofview] goals come with a stateMaxime Dénès
2018-03-04Merge PR #915: Fix rewrite in * side conditionsMaxime Dénès
2018-03-04Merge PR #6735: [toplevel] [vernac] Remove Load hack and check / document ↵Maxime Dénès
supported scenarios.
2018-03-02[VM] Unify Const_sorts and Const_type, and remove Vsort.Maxime Dénès
This simplifies the representation of values, and brings it closer to the ones of the native compiler.
2018-03-02[stm] Partial fix for bug #6884 [location missing from replay nodes]Emilio Jesus Gallego Arias
Example not yet fixed by this patch: ``` Definition u : Type. Definition m : Type. exact nat. Defined. exact bool. Defined. ```
2018-03-01Harden gitattributes against core.whitespace configuration.Gaëtan Gilbert
2018-03-01Fix #6878: univ undefined for [with Definition] bad instance size.Gaëtan Gilbert
2018-03-01Fixing rewriting in side conditions for "rewrite in *" and "rewrite in * |-".Hugo Herbelin
Noticed by Sigurd Schneider.
2018-03-01Moving code for "simple induction"/"simple destruct" to coretactics.ml4.Hugo Herbelin
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-28[toplevel] Update state when `Drop` exception is thrown [#6872]Emilio Jesus Gallego Arias
`Drop` is implemented using exceptions-as-control flow, so the toplevel state gets corrupted as `do_vernac` will never return when `Drop` occurs in the input. The right fix would be to remove `Drop` from the vernacular and make it a toplevel-only command, but meanwhile we can just patch the state in the exception handler. We also need to keep the global state in `Coqloop` as the main `coqtop` entry point won't be called by `go ()`. Fixes #6872.
2018-02-28[toplevel] Move beautify to its own pass.Emilio Jesus Gallego Arias
We first load the file, then we print it as a post-processing step. This is both more flexible and clearer. We also refactor the comments handling to minimize the logic that is living in the Lexer. Indeed, the main API is now living in the printer, and complex interactions with the state are not possible anymore, including the removal of messing with low-level summary and state setting!
2018-02-28[test-suite] Add a basic test-case for `Load`.Emilio Jesus Gallego Arias
We test the 3 possible scenarios. A more complete test would also involved fake_ide. c.f. #6793
2018-02-28[toplevel] [vernac] Remove Load hack and check supported scenarios.Emilio Jesus Gallego Arias
Parsing in `VernacLoad` was broken for a while, but the situation has improved by miscellaneous refactoring. However, we still cannot support `Load` properly when proofs are crossing file boundaries. So in this patch we do two things: - We check for supported scenarios [no proofs open at `Load` entry/exit] - Remove the hack in `toplevel` so the behavior of `Load` is consistent between `coqide`/`coqc`. We close #5053 as its main bug was fixed by the main toplevel refactoring and the remaining cases are documented now.
2018-02-28[econstr] Continue consolidation of EConstr API under `interp`.Emilio Jesus Gallego Arias
This commit was motivated by true spurious conversions arising in my `to_constr` debug branch. The changes here need careful review as the tradeoffs are subtle and still a lot of clean up remains to be done in `vernac/*`. We have opted for penalize [minimally] the few users coming from true `Constr`-land, but I am sure we can tweak code in a much better way. In particular, it is not clear if internalization should take an `evar_map` even in the cases where it is not triggered, see the changes under `plugins` for a good example. Also, the new return type of `Pretyping.understand` should undergo careful review. We don't touch `Impargs` as it is not clear how to proceed, however, the current type of `compute_implicits_gen` looks very suspicious as it is called often with free evars. Some TODOs are: - impargs was calling whd_all, the Econstr equivalent can be either + Reductionops.whd_all [which does refolding and no sharing] + Reductionops.clos_whd_flags with all as a flag.
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-30 04:56:53 +0000