aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* Merge PR #6900: [compat] Remove "Tactic Pattern Unification"Gravatar Maxime Dénès2018-03-06
|\
* \ Merge PR #6898: [compat] Remove "Intuition Iff Unfolding"Gravatar Maxime Dénès2018-03-06
|\ \
* \ \ Merge PR #6901: [compat] Remove "Injection L2R Pattern Order"Gravatar Maxime Dénès2018-03-06
|\ \ \
* \ \ \ Merge PR #6855: Update headers following #6543.Gravatar Maxime Dénès2018-03-05
|\ \ \ \
* \ \ \ \ Merge PR #6700: [ssr] rewrite Ssripats and Ssrview in the tactic monadGravatar Maxime Dénès2018-03-05
|\ \ \ \ \
* \ \ \ \ \ Merge PR #935: Handling evars in the VMGravatar Maxime Dénès2018-03-04
|\ \ \ \ \ \
| | * | | | | ssr: ipats: V82.tactic ~nf_evars:false everywhereGravatar Enrico Tassi2018-03-04
| | | | | | |
| | * | | | | Proofview: V82.tactic option to not normalize evarsGravatar Enrico Tassi2018-03-04
| | | | | | |
| | * | | | | ssr: rewrite Ssripats and Ssrview in the tactic monadGravatar Enrico Tassi2018-03-04
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Ssripats and Ssrview are now written in the Tactic Monad. Ssripats implements the => tactical. Ssrview implements the application of forward views. The code is, according to my tests, 100% backward compatible. The code is much more documented than before. Moreover the "ist" (ltac context) used to interpret views is the correct one (the one at ARGUMENT EXTEND interp time, not the one at TACTIC EXTEND execution time). Some of the code not touched by this commit still uses the incorrect ist, so its visibility in TACTIC EXTEND can't be removed yet. The main changes in the code are: - intro patterns are implemented using a state machine (a goal comes with a state). Ssrcommon.MakeState provides an easy way for a tactic to enrich the goal with with data of interest, such as the set of hyps to be cleared. This cleans up the old implementation that, in order to thread the state, that to redefine a bunch of tclSTUFF - the interpretation of (multiple) forward views uses the state to accumulate intermediate results - the bottom of Sscommon collects a bunch of utilities written in the tactic monad. Most of them are the rewriting of already existing utilities. When possible the old version was removed.
| | * | | | | tactics: export e_reduct_in_conclGravatar Enrico Tassi2018-03-04
| | | | | | |
| | * | | | | reductionops: remove dead code "bind_assum"Gravatar Enrico Tassi2018-03-04
| | | | | | |
| | * | | | | proofview: debug API to print a goalGravatar Enrico Tassi2018-03-04
| | | | | | |
* | | | | | | Merge PR #6791: Removing compatibility support for versions older than 8.5.Gravatar Maxime Dénès2018-03-04
|\ \ \ \ \ \ \
* \ \ \ \ \ \ \ Merge PR #6736: [toplevel] Move beautify to its own pass.Gravatar Maxime Dénès2018-03-04
|\ \ \ \ \ \ \ \ | |_|_|/ / / / / |/| | | | | | |
* | | | | | | | Merge PR #6511: [econstr] Continue consolidation of EConstr API under `interp`.Gravatar Maxime Dénès2018-03-04
|\ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ Merge PR #6876: Unify Const_sorts and Const_type, and remove VsortGravatar Maxime Dénès2018-03-04
|\ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ Merge PR #6846: Moving code for "simple induction"/"simple destruct" to ↵Gravatar Maxime Dénès2018-03-04
|\ \ \ \ \ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | coretactics.ml4.
* \ \ \ \ \ \ \ \ \ \ Merge PR #6885: [stm] Partial fix for bug #6884 [location missing from ↵Gravatar Maxime Dénès2018-03-04
|\ \ \ \ \ \ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | replay nodes]
* \ \ \ \ \ \ \ \ \ \ \ Merge PR #6873: [toplevel] Update state when `Drop` exception is thrown [#6872]Gravatar Maxime Dénès2018-03-04
|\ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #6882: Harden gitattributes against core.whitespace configuration.Gravatar Maxime Dénès2018-03-04
|\ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #6879: Fix #6878: univ undefined for [with Definition] bad instance ↵Gravatar Maxime Dénès2018-03-04
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | size.
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #6676: [proofview] goals come with a stateGravatar Maxime Dénès2018-03-04
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #915: Fix rewrite in * side conditionsGravatar Maxime Dénès2018-03-04
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #6735: [toplevel] [vernac] Remove Load hack and check / document ↵Gravatar Maxime Dénès2018-03-04
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | supported scenarios.
| | | | | | | | | | | | | * | | | | Removing test for bug #2850.Gravatar Pierre-Marie Pédrot2018-03-03
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This test was actually checking that evar-containing terms were making the VM fail. Obviously this is not the case anymore, so the test is now invalid.
| | | | | | | | | | | | | * | | | | Adding a test file for evar handling in the VM.Gravatar Pierre-Marie Pédrot2018-03-03
| | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | * | | | | Handling evars in the VM.Gravatar Pierre-Marie Pédrot2018-03-03
| |_|_|_|_|_|_|_|_|_|_|_|/ / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We simply treat them as as an application of an atom to its instance, and in the decompilation phase we reconstruct the instance from the stack. This grants wish BZ#5659.
| | | | | | | | | | | | | | | | * [compat] Remove "Tactic Pattern Unification"Gravatar Emilio Jesus Gallego Arias2018-03-03
| |_|_|_|_|_|_|_|_|_|_|_|_|_|_|/ |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Following up on #6791, we remove the option "Tactic Pattern Unification"
| | | | | | | | | | | | | | | * [compat] Remove "Intuition Iff Unfolding"Gravatar Emilio Jesus Gallego Arias2018-03-03
| |_|_|_|_|_|_|_|_|_|_|_|_|_|/ |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Following up on #6791, we remove the option "Intuition Iff Unfolding"
| | | | | | | | | | | | | | * [compat] Remove "Injection L2R Pattern Order"Gravatar Emilio Jesus Gallego Arias2018-03-03
| |_|_|_|_|_|_|_|_|_|_|_|_|/ |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Following up on #6791, we remove the option "Injection L2R Pattern Order".
| | | | | | | | | | | | * | CHANGES entry for #6791.Gravatar Théo Zimmermann2018-03-02
| | | | | | | | | | | | | |
| | | | | | | | | | | | * | Remove 8.5 compatibility support.Gravatar Théo Zimmermann2018-03-02
| | | | | | | | | | | | | |
| | | | | | | | | | | | * | Remove VOld compatibility flag.Gravatar Théo Zimmermann2018-03-02
| | | | | | | | | | | | | |
| | | | | | | | | | | | * | Turn warning for deprecated notations on.Gravatar Théo Zimmermann2018-03-02
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Fix new deprecation warnings in the standard library.
| | | | | | | | | | | | * | Remove the deprecation for some 8.2-8.5 compatibility aliases.Gravatar Théo Zimmermann2018-03-02
| |_|_|_|_|_|_|_|_|_|_|/ / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
| | | | | | | | | * | | | [VM] Unify Const_sorts and Const_type, and remove Vsort.Gravatar Maxime Dénès2018-03-02
| |_|_|_|_|_|_|_|/ / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This simplifies the representation of values, and brings it closer to the ones of the native compiler.
| | | | | | | * | | | | [stm] Partial fix for bug #6884 [location missing from replay nodes]Gravatar Emilio Jesus Gallego Arias2018-03-02
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Example not yet fixed by this patch: ``` Definition u : Type. Definition m : Type. exact nat. Defined. exact bool. Defined. ```
| | | | | * | | | | | | Harden gitattributes against core.whitespace configuration.Gravatar Gaëtan Gilbert2018-03-01
| |_|_|_|/ / / / / / / |/| | | | | | | | | |
| | | | * | | | | | | Fix #6878: univ undefined for [with Definition] bad instance size.Gravatar Gaëtan Gilbert2018-03-01
| |_|_|/ / / / / / / |/| | | | | | | | |
| | * | | | | | | | 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.
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-27 01:29:13 +0000