aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
...
| | * | | | | | | | | Fixing rewriting in side conditions for "rewrite in *" and "rewrite in * |-".Gravatar Hugo Herbelin2018-03-01
| | | |_|/ / / / / / | | |/| | | | | | | | | | | | | | | | | | | | | | | | | | | Noticed by Sigurd Schneider.
| | | | | * | | | | Moving code for "simple induction"/"simple destruct" to coretactics.ml4.Gravatar Hugo Herbelin2018-03-01
| | | | | | | | | |
* | | | | | | | | | Merge PR #6856: travis: elpi needs findlib >= 1.5Gravatar Maxime Dénès2018-03-01
|\ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ Merge PR #6864: Remove empty, wrongly located, doc file.Gravatar Maxime Dénès2018-03-01
|\ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ Merge PR #6861: Typo in the documentation of the `pattern` tacticGravatar Maxime Dénès2018-03-01
|\ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #6850: Fix #6751 trust_file_cache logic was invertedGravatar Maxime Dénès2018-03-01
|\ \ \ \ \ \ \ \ \ \ \ \ \
| | | | | | | | * | | | | | [toplevel] Update state when `Drop` exception is thrown [#6872]Gravatar Emilio Jesus Gallego Arias2018-02-28
| | | | | | | |/ / / / / / | | | | | | |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | `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.
| | | | | | | | | | * | | [toplevel] Move beautify to its own pass.Gravatar Emilio Jesus Gallego Arias2018-02-28
| | | | | | |_|_|_|/ / / | | | | | |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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!
| | | | | * | | | | | | [test-suite] Add a basic test-case for `Load`.Gravatar Emilio Jesus Gallego Arias2018-02-28
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We test the 3 possible scenarios. A more complete test would also involved fake_ide. c.f. #6793
| | | | | * | | | | | | [toplevel] [vernac] Remove Load hack and check supported scenarios.Gravatar Emilio Jesus Gallego Arias2018-02-28
| | | | | |/ / / / / / | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
| | | | | | | | * / / [econstr] Continue consolidation of EConstr API under `interp`.Gravatar Emilio Jesus Gallego Arias2018-02-28
| | | | | | |_|/ / / | | | | | |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
| | | | * | | | | | travis: elpi needs findlib >= 1.5Gravatar Enrico Tassi2018-02-28
| | | | | | | | | |
| | | | * | | | | | tavis: make the . in pkg.version part of $VERSIONGravatar Enrico Tassi2018-02-28
| | | | | | | | | |
* | | | | | | | | | Merge PR #6847: Fix make source-docGravatar Maxime Dénès2018-02-28
|\ \ \ \ \ \ \ \ \ \ | |_|_|_|_|/ / / / / |/| | | | | | | | |
* | | | | | | | | | Merge PR #6854: comment "resolvability" bit in Evd.evar_mapGravatar Maxime Dénès2018-02-28
|\ \ \ \ \ \ \ \ \ \ | |_|_|_|_|_|_|/ / / |/| | | | | | | | |
* | | | | | | | | | Merge PR #6852: [stdlib] move “Require” out of sectionsGravatar Maxime Dénès2018-02-28
|\ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ Merge PR #6853: Add a comment on EConstr.to_constr regarding evar-freeness.Gravatar Maxime Dénès2018-02-28
|\ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ Merge PR #1026: changed statements of Rpower_lt and Rle_power and added lemmasGravatar Maxime Dénès2018-02-28
|\ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #6756: Fix issue with spurious timing test failuresGravatar Maxime Dénès2018-02-28
|\ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #6788: Fixes #6787 (minus sign interpreted by coqdoc as a bullet in ↵Gravatar Maxime Dénès2018-02-28
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Ring_theory.v)
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #6789: Check whitespace errors per-commit.Gravatar Maxime Dénès2018-02-28
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #6734: dest_{prod,lam}: no Cast case (it's removed by whd)Gravatar Maxime Dénès2018-02-28
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #6823: Fixes #6821 (bug in protecting notation printing from ↵Gravatar Maxime Dénès2018-02-28
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | infinite eta-expansion)
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #6812: Rename release_lexer_state to the more descriptive ↵Gravatar Maxime Dénès2018-02-28
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | get_lexer_state.
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #6752: Remove from CircleCI builds that are already taken care of ↵Gravatar Maxime Dénès2018-02-28
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |_|_|_|_|_|_|_|_|_|_|_|_|_|_|/ / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | by Travis.
| | | | | | | | | | | | | | | * | | | Remove empty, wrongly located, doc file.Gravatar Théo Zimmermann2018-02-28
| |_|_|_|_|_|_|_|_|_|_|_|_|_|/ / / / |/| | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | * | | | Typo in the documentation of the `pattern` tacticGravatar Joachim Breitner2018-02-27
| |_|_|_|_|_|_|_|_|_|_|_|_|/ / / / |/| | | | | | | | | | | | | | | |
| | | | | | | | | | | * | | | | | comment "resolvability" bit in Evd.evar_mapGravatar Enrico Tassi2018-02-27
| |_|_|_|_|_|_|_|_|_|/ / / / / / |/| | | | | | | | | | | | | | |
| | | | | | | | | | | | | | * | Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
| |_|_|_|_|_|_|_|_|_|_|_|_|/ / |/| | | | | | | | | | | | | |
| | | | | | | | | | | | * | | Fix #6751 trust_file_cache logic was invertedGravatar Gaëtan Gilbert2018-02-27
| |_|_|_|_|_|_|_|_|_|_|/ / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Bug introduced by 675a1dc401eb9a5540ba5bc9a522c1f84d4c3d54
| | | | | | | | | * | | | | Add a comment on EConstr.to_constr regarding evar-freeness.Gravatar Pierre-Marie Pédrot2018-02-27
| |_|_|_|_|_|_|_|/ / / / / |/| | | | | | | | | | | |
| | | | | | | | | * | | | [stdlib] move “Require” out of sectionsGravatar Vincent Laporte2018-02-27
| |_|_|_|_|_|_|_|/ / / / |/| | | | | | | | | | |
| | | | | | | | | * | | Use relative path for show_latex_messagesGravatar mrmr19932018-02-27
| | | | | | | | | | | |
| | | | | | | | | * | | Use MYCAMLP5LIB instead of undefined MYCAMLP4LIBGravatar mrmr19932018-02-27
| |_|_|_|_|_|_|_|/ / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This completes the work of b60906cc3ee3f994babf9cceff2971bd03485f2f
| | | | | | | * | | | [test-suite] Move sed scripts into bash arraysGravatar Jason Gross2018-02-24
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | As per https://github.com/coq/coq/pull/6756/files#r168028764
* | | | | | | | | | | Merge PR #6543: Update headers and creditsGravatar Maxime Dénès2018-02-24
|\ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ Merge PR #6784: New IR in VM: ClambdaGravatar Maxime Dénès2018-02-24
|\ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #6819: Document Arguments extra scopes flagGravatar Maxime Dénès2018-02-24
|\ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #6776: Fixes bug #6774 (anomaly with ill-typed template polymorphism).Gravatar Maxime Dénès2018-02-24
|\ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #6803: coqdev.el: add space at the end of compile-commandGravatar Maxime Dénès2018-02-24
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #6599: Decimals in preludeGravatar Maxime Dénès2018-02-24
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #6745: [ast] Improve precision of Ast location recognition in ↵Gravatar Maxime Dénès2018-02-24
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | serialization.
| | | | | | | | | | | | * | | | | | Check whitespace errors per-commit.Gravatar Gaëtan Gilbert2018-02-23
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Otherwise it is possible to detect errors that are not fixed by git rebase since that works per-commit.
| | | | | | * | | | | | | | | | | | New IR in VM: Clambda.Gravatar Maxime Dénès2018-02-23
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
| | | | | | * | | | | | | | | | | | Fix map iterator on nativelambda.Gravatar Maxime Dénès2018-02-23
| | | | | | | |_|_|_|_|/ / / / / / | | | | | | |/| | | | | | | | | |
| | | | | | | | | | * | | | | | | Fixes #6821 (bug in protecting notation printing from infinite eta-expansion).Gravatar Hugo Herbelin2018-02-23
| |_|_|_|_|_|_|_|_|/ / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
| | | | | * | | | | | | | | | | Document Arguments extra scopes flagGravatar Jasper Hugunin2018-02-22
| |_|_|_|/ / / / / / / / / / / |/| | | | | | | | | | | | | |
| | | | | | | | * | | | | | | Tweak developer documentation.Gravatar Jim Fehrle2018-02-22
| | | | | | | | | | | | | | |
| | | | | | | | * | | | | | | Rename release_lexer_state to the more descriptive get_lexer_state.Gravatar Jim Fehrle2018-02-22
| | | | | | |_|/ / / / / / / | | | | | |/| | | | | | | |
| * | | | / | | | | | | | | [ast] Improve precision of Ast location recognition in serialization.Gravatar Emilio Jesus Gallego Arias2018-02-22
|/ / / / / / / / / / / / / | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-01 23:18:12 +0000