aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2019-04-12Merge PR #9949: [stm] Report correct ids on some errors where it was dummy.Enrico Tassi
Reviewed-by: gares
2019-04-12Remove `constr_of_global_in_context`Maxime Dénès
This function seems unused.
2019-04-12Unify Set and Unset handling for optionsGaëtan Gilbert
Not sure if the idetop.set_options was correctly changed, ocaml types pass at least.
2019-04-11[stm] Report correct ids on some errors where it was dummy.Shachar Itzhaky
2019-04-11Merge pull request coq/ltac2#119 from maximedenes/pretyping-rm-globalPierre-Marie Pédrot
Adapt to Coq's PR #9909
2019-04-11Merge PR #9909: Remove all but one call to `Global` in the pretyperPierre-Marie Pédrot
Ack-by: ejgallego Reviewed-by: gares Ack-by: maximedenes Ack-by: ppedrot
2019-04-11Merge PR #9938: [coqdep] Exit with error code on exception.Pierre-Marie Pédrot
Reviewed-by: ppedrot
2019-04-10Merge PR #9943: [mailmap] Tweak Emilio's entries.Théo Zimmermann
Reviewed-by: Zimmi48
2019-04-10Merge PR #9910: [api] [proofs] Remove dependency of proofs on interp.Gaëtan Gilbert
Reviewed-by: SkySkimmer
2019-04-10Overlays for Global removal in pretyperMaxime Dénès
2019-04-10Remove calls to Global.env in HeadsMaxime Dénès
2019-04-10Remove calls to global env in InductiveopsMaxime Dénès
2019-04-10Remove calls to Global.env from EvarsolveMaxime Dénès
2019-04-10Remove calls to Global.env and Libobject from RecordopsMaxime Dénès
2019-04-10Remove calls to Global.env in TypingMaxime Dénès
2019-04-10Remove calls to Global.env in Glob_opsMaxime Dénès
2019-04-10Remove calls to Global.env in PatternopsMaxime Dénès
2019-04-10Remove call to global env in pretyping.mlMaxime Dénès
2019-04-10Functionalize env in type classesMaxime Dénès
I had to reorganize the code a bit. The Context command moved to comAssumption, as it is not so related to type classes. We were able to remove a few hooks on the way.
2019-04-10Move vernac-related part of coercions to vernacMaxime Dénès
2019-04-10Remove one call to Global.env in DetypingMaxime Dénès
One other call still remains, but will require to refactor some section-handling code.
2019-04-10Remove calls to global env from indrecMaxime Dénès
2019-04-10Fix constant order in heads.mlMaxime Dénès
As per the OCaml documentation, the order for maps should be total. I also remove some circumvolutions that were added around eliminators and canonical names because of this incorrect order.
2019-04-10[mailmap] Tweak Emilio's entries.Emilio Jesus Gallego Arias
2019-04-10Merge PR #9941: Improve SProp error message to mention the Allow StrictProp ↵Gaëtan Gilbert
flag. Reviewed-by: SkySkimmer
2019-04-10Improve SProp error message to mention the Allow StrictProp flag.Théo Zimmermann
And document the error message.
2019-04-10[coqdep] Exit with error code on exception.Emilio Jesus Gallego Arias
This turns out to confuse many tools otherwise.
2019-04-09[api] [proof] Alert users that `Vernacstate.Proof_global` is not to be used.Emilio Jesus Gallego Arias
We alert users that `Vernacstate.Proof_global` is a Coq internal module and should not be used to workaround lack of state threading.
2019-04-09Merge PR #9928: Fix #9812: CoqIDE on gtk3 has wrong defaults for selection BG.Enrico Tassi
Reviewed-by: gares
2019-04-09Merge PR #9931: Fix spelling in comment.Théo Zimmermann
Reviewed-by: Zimmi48
2019-04-09Adapt to Coq's PR #9909Maxime Dénès
2019-04-09Add a few missing notes to the release doc.Théo Zimmermann
2019-04-08Fix spelling in comment.nlewycky
Fix spelling (French fonction --> English function).
2019-04-08Fix #9812: CoqIDE on gtk3 has wrong defaults for selection BG.Pierre-Marie Pédrot
Unfortunately, the only sane fix I was able to hack was to deactivate the possibility to change the background colour altogether. Trying to do otherwise is a real Pandora's box which is ultimately triggered by the lack of lablgtk3 bindings for the GtkStyleContext class. I tried a lot of alternative approaches, to no avail. This includes catching the selection signal, reimplementing selection by hand in GtkTextView, and even reading the internal details of the GTK implementation turned not that helpful. For the time being (8.10 beta) I think we do not have much choice.
2019-04-08Don't store closures in summary (reduction effects)Gaëtan Gilbert
We already have indirection (constant -> effect name, effect name -> function) so we only need to stop using summary.ref for the second map.
2019-04-08Merge PR #9915: Remove cache in HeadsEnrico Tassi
Reviewed-by: gares
2019-04-08coq_makefile install target: error if any file is missingGaëtan Gilbert
2019-04-08Merge PR #9900: [native compiler] Fix critical bug with stuck primitive ↵Pierre-Marie Pédrot
projections Ack-by: SkySkimmer Reviewed-by: Zimmi48 Ack-by: maximedenes Reviewed-by: ppedrot
2019-04-06Merge PR #9924: Fix numeral notations test in async mode.Emilio Jesus Gallego Arias
2019-04-06Fix numeral notations test in async mode.Gaëtan Gilbert
Async causes output reordering in one test. Since we don't care about the output of that test (it's just a [Fail]) we move it to success/.
2019-04-06Merge PR #9923: [ci/deploy] Fix branch creation when pushing to ↵Emilio Jesus Gallego Arias
coq/coq-on-cachix. Reviewed-by: ejgallego
2019-04-06Fix pretty-printing of primitive integersErik Martin-Dorel
A scope delimiter was missing for primitive integers constants. Add related regression tests.
2019-04-06[ci/deploy] Fix branch creation when pushing to coq/coq-on-cachix.Théo Zimmermann
2019-04-05[native compiler] Fix critical bug with primitive projectionsMaxime Dénès
Since e1e7888, stuck projections were not computed correctly. Fixes #9684
2019-04-05[native compiler] Normalize before destructuring sortMaxime Dénès
This was making an assertion fail on https://github.com/coq/coq/issues/9684 after 23f84f37
2019-04-05[api] [proofs] Remove dependency of proofs on interp.Emilio Jesus Gallego Arias
We perform some cleanup and remove dependency of `proofs/` on `interp/`, which seems logical. In fact, `interp` + `parsing` are quite self-contained, so if there is interest we could also make tactics to depend directly on proofs.
2019-04-05Merge PR #9685: [vernac] Small cleanup to remove assert false.Vincent Laporte
Ack-by: SkySkimmer Ack-by: ejgallego Reviewed-by: vbgl
2019-04-05Remove cache in HeadsMaxime Dénès
This cache makes the pretyper depend on components that should morally be higher-level (Libobject and co), so I'd like to see how critical this cache is before taking any action.
2019-04-05Merge pull request coq/ltac2#116 from proux01/master-parsing-decimalPierre-Marie Pédrot
[coq] Adapt to coq/coq#8764
2019-04-05Merge PR #8764: Add parsing of decimal constants (e.g., 1.02e+01)Emilio Jesus Gallego Arias
Reviewed-by: Zimmi48 Reviewed-by: ejgallego Ack-by: gares Ack-by: herbelin Ack-by: ppedrot Ack-by: proux01
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-20 11:17:38 +0000