aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2020-05-16Merge PR #11566: [misc] Better preserve backtraces in several modulesPierre-Marie Pédrot
Ack-by: SkySkimmer Reviewed-by: ppedrot
2020-05-15Merge PR #12239: Split Gallina, Gallina ext and most of CIC chapters into ↵Clément Pit-Claudel
multiple pages. Reviewed-by: jfehrle
2020-05-15Merge PR #12323: Fixes #12322: anomaly when printing "fun" binders with ↵Emilio Jesus Gallego Arias
implicit types Reviewed-by: ejgallego
2020-05-15Merge PR #11979: Add a rudimentary script to generate release changelog.Emilio Jesus Gallego Arias
Ack-by: SkySkimmer Reviewed-by: ejgallego
2020-05-15Merge PR #11948: Hexadecimal numeralsHugo Herbelin
Reviewed-by: JasonGross Ack-by: Zimmi48 Ack-by: herbelin
2020-05-15Merge PR #11755: [exn] [tactics] improve backtraces on monadic errorsPierre-Marie Pédrot
Ack-by: gares Ack-by: ppedrot
2020-05-15Merge PR #12243: Add a note on build-time dependencies to INSTALL.md.Emilio Jesus Gallego Arias
Ack-by: JasonGross Ack-by: SkySkimmer Reviewed-by: cpitclaudel Reviewed-by: ejgallego Ack-by: ppedrot
2020-05-15Fix typo.Théo Zimmermann
2020-05-15Merge PR #11992: do not re-export ListNotations from ProgramAnton Trunov
Reviewed-by: Zimmi48 Reviewed-by: anton-trunov Reviewed-by: ejgallego
2020-05-15Merge PR #12032: [win] Elpi, Coq-Elpi and HBMichael Soegtrop
Reviewed-by: MSoegtropIMC
2020-05-15[interp] Register printers for InternalizationError instead of ad-hoc hanlding.Emilio Jesus Gallego Arias
2020-05-15[misc] Better preserve backtraces in several modulesEmilio Jesus Gallego Arias
Re-raising inside exception handlers must be done with care in order to preserve backtraces; even if newer OCaml versions do a better job in automatically spilling `%reraise` in places that matter, there is no guarantee for that to happen. I've done a best-effort pass of places that were re-raising incorrectly, hopefully I got the logic right. There is the special case of `Nametab.error_global_not_found` which is raised many times in response to a `Not_found` error; IMHO this error should be converted to something more specific, however the scope of that change would be huge as to do easily...
2020-05-14Merge PR #12256: Move the static check of evaluability in unfold tactic to ↵Hugo Herbelin
runtime. Reviewed-by: herbelin
2020-05-14[exn] [tactics] improve backtraces on monadic errorsEmilio Jesus Gallego Arias
Current backtraces for tactics leave a bit to desire, for example given the program: ```coq Lemma u n : n + 0 = n. rewrite plus_O_n. ``` the backtrace stops at: ``` Found no subterm matching "0 + ?M160" in the current goal. Called from file "proofs/proof.ml", line 381, characters 4-42 Called from file "tactics/pfedit.ml", line 102, characters 31-58 Called from file "plugins/ltac/g_ltac.mlg", line 378, characters 8-84 ``` Backtrace information `?info` is as of today optional in some tactics, such as `tclZERO`, it doesn't cost a lot however to reify backtrace information indeed in `tclZERO` and provide backtraces for all tactic errors. The cost should be small if we are not in debug mode. The backtrace for the failed rewrite is now: ``` Found no subterm matching "0 + ?M160" in the current goal. Raised at file "pretyping/unification.ml", line 1827, characters 14-73 Called from file "pretyping/unification.ml", line 1929, characters 17-53 Called from file "pretyping/unification.ml", line 1948, characters 22-72 Called from file "pretyping/unification.ml", line 2020, characters 14-56 Re-raised at file "pretyping/unification.ml", line 2021, characters 66-73 Called from file "proofs/clenv.ml", line 254, characters 12-58 Called from file "proofs/clenvtac.ml", line 95, characters 16-53 Called from file "engine/proofview.ml", line 1110, characters 40-46 Called from file "engine/proofview.ml", line 1115, characters 10-34 Re-raised at file "clib/exninfo.ml", line 82, characters 4-38 Called from file "proofs/proof.ml", line 381, characters 4-42 Called from file "tactics/pfedit.ml", line 102, characters 31-58 Called from file "plugins/ltac/g_ltac.mlg", line 378, characters 8-84 ``` which IMO is much better.
2020-05-14Add advisories on OCaml setup to INSTALL.md.Théo Zimmermann
Closes #12232.
2020-05-14Merge PR #12296: Fixes #12234: wrong environment for Show ProofGaëtan Gilbert
Reviewed-by: SkySkimmer
2020-05-14Merge PR #12327: Add a changelog for 8.11.2.Théo Zimmermann
Reviewed-by: Zimmi48
2020-05-14Merge PR #11922: No more local reduction functions in Reductionops.Maxime Dénès
Reviewed-by: Matafou Ack-by: SkySkimmer Reviewed-by: gares
2020-05-14Add a changelog for 8.11.2.Pierre-Marie Pédrot
2020-05-14Merge PR #12312: Clarify the documentation for merging PRs with overlaysThéo Zimmermann
Reviewed-by: Zimmi48
2020-05-14Fix title level and a build failure.Théo Zimmermann
2020-05-14Fix conflicts with latest master.Théo Zimmermann
2020-05-14Add some markers of origin.Théo Zimmermann
2020-05-14Reintroduce leftover parts; update index files; small fixes.Théo Zimmermann
2020-05-14Adding changelog.Pierre-Marie Pédrot
2020-05-14Remove an outdated piece of documentation about limitations of unfold.Pierre-Marie Pédrot
2020-05-14Tweak the error message of reference internalization.Pierre-Marie Pédrot
2020-05-14Add test for #11727, which was indirectly fixed by this PR.Pierre-Marie Pédrot
2020-05-14Generalize the interpretation of syntactic notation as reference to their head.Pierre-Marie Pédrot
This seems to be a pattern used quite a bit in the wild, it does not hurt to be a bit more lenient to tolerate this kind of use. Interestingly the API was already offering a similar generalization in some unrelated places. We also backtrack on the change in Floats.FloatLemmas since it is an instance of this phenomenon.
2020-05-14Move the static check of evaluability in unfold tactic to runtime.Pierre-Marie Pédrot
See #11840 for a motivation. I had to fix Floats.FloatLemmas because it uses the same name for a notation and a term, and the fact this unfold was working on this was clearly a bug. I hope nobody relies on this kind of stuff in the wild. Fixes #5764: "Cannot coerce ..." should be a runtime error. Fixes #5159: "Cannot coerce ..." should not be an error. Fixes #4925: unfold gives error on Admitted.
2020-05-14Added change log.Hugo Herbelin
2020-05-14Fixes #12234 (wrong environment for Show Proof).Hugo Herbelin
We take the env of the current goal with the context replaced with section variables. In practice, this is the global env, but, maybe, one day, a goal state will have its own env.
2020-05-14Refactoring of the first part of the reference manual.Théo Zimmermann
2020-05-14Preserve Implicit arguments file.Théo Zimmermann
2020-05-14Remove Canonical structures from Implicit arguments.Théo Zimmermann
2020-05-14Merge doc on Canonical structures from two origins.Théo Zimmermann
2020-05-14Merge PR #12313: Make explicit that UGraph lower bounds are only of two kinds.Gaëtan Gilbert
Reviewed-by: SkySkimmer
2020-05-14Move Canonical structures file into new location.Théo Zimmermann
2020-05-14Merge PR #12320: [ci] [sf] Fix SF build.Gaëtan Gilbert
Reviewed-by: SkySkimmer
2020-05-14Add Canonical structure declarations to Canonical structures file.Théo Zimmermann
2020-05-14Extract Canonical structures from Implicit arguments.Théo Zimmermann
2020-05-14Split Gallina extensions into multiple files.Théo Zimmermann
2020-05-14Split Gallina into multiple files.Théo Zimmermann
2020-05-14Split parts of CIC into multiple files.Théo Zimmermann
2020-05-14Create new file on Functions and Assumptions.Théo Zimmermann
2020-05-14Extract functions and assumptions.Théo Zimmermann
2020-05-14Merge definitions and type casts in same file.Théo Zimmermann
2020-05-14Create new file on Definitions.Théo Zimmermann
2020-05-14Extract Definitions from Gallina.Théo Zimmermann
2020-05-14Add type casts to new Definitions file.Théo Zimmermann
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-28 04:16:15 +0000