aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2019-04-12Remove `constr_of_global_in_context`Maxime Dénès
This function seems unused.
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-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-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-08Merge PR #9915: Remove cache in HeadsEnrico Tassi
Reviewed-by: gares
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-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 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
2019-04-04Update CHANGES.mdPierre Roux
2019-04-04Merge PR #9904: [CI] Fix build of math-comp dependenciesGaëtan Gilbert
Reviewed-by: SkySkimmer Reviewed-by: gares
2019-04-04[CI] Fix build of math-comp dependenciesMaxime Dénès
We were incorrectly calling the global `install` target even when building only subcomponents of the library.
2019-04-04Merge PR #9901: [dune] Fix include object dirs.Théo Zimmermann
Reviewed-by: Zimmi48
2019-04-04[dune] Fix include object dirs.Emilio Jesus Gallego Arias
In Dune >= 1.8 object dirs have changed; this should be stable for a while, however we want a more robust setup for sure, which I think it should be able to be implemented when we have a single build system.
2019-04-04Merge PR #9881: Protect some I/O routines from SIGALRMEmilio Jesus Gallego Arias
Ack-by: SkySkimmer Reviewed-by: ejgallego Ack-by: maximedenes
2019-04-03Merge PR #9890: Improve coqchk -norec perf by not checking for ill-formed ↵Pierre-Marie Pédrot
data in dependencies Reviewed-by: ppedrot
2019-04-03Merge PR #9804: CI: Use job-local timeout for build-template and ↵Emilio Jesus Gallego Arias
test-suite-template Reviewed-by: ejgallego Reviewed-by: gares
2019-04-03Merge PR #9861: [program] Allow evars in type of fixpoints.Gaëtan Gilbert
Reviewed-by: SkySkimmer
2019-04-03Protect some I/O routines from SIGALRMMaxime Dénès
This is necessary to prevent Coq from sending ill-formed output in some scenarios involving `Timeout`. Co-authored-by: Enrico Tassi <Enrico.Tassi@inria.fr>
2019-04-03Merge PR #9078: Provide a faster bound name generation algorithm through a flagVincent Laporte
Ack-by: jfehrle Ack-by: ppedrot Reviewed-by: vbgl
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-28 14:53:16 +0000