aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2019-04-16[doc] Changes for coq/coq#9165Emilio Jesus Gallego Arias
2019-04-16[ci] Overlays for coq/coq#9165Emilio Jesus Gallego Arias
2019-04-16[ast] [constrexpr] Make recursion_order_expr an AST node.Emilio Jesus Gallego Arias
This is a bit more uniform.
2019-04-16Update and fix documentation of Program Fixpoint with measureMaxime Dénès
2019-04-16Fix spurious argument of {measure}Maxime Dénès
Previsouly, it was silently ignored.
2019-04-16Take advantage of relaxed {measure} syntax in test suiteMaxime Dénès
2019-04-16Clean the representation of recursive annotation in ConstrexprMaxime Dénès
We make clearer which arguments are optional and which are mandatory. Some of these representations are tricky because of small differences between Program and Function, which share the same infrastructure. As a side-effect of this cleanup, Program Fixpoint can now be used with e.g. {measure (m + n) R}. Previously, parentheses were required around R.
2019-04-15Merge PR #9927: Don't store closures in summary (reduction effects)Pierre-Marie Pédrot
Reviewed-by: ppedrot
2019-04-15Merge PR #9959: [native compiler] Remove `Lconstruct` from lambda code.Pierre-Marie Pédrot
Ack-by: maximedenes Reviewed-by: ppedrot
2019-04-14[native compiler] Remove now unused GconstructMaxime Dénès
2019-04-14[native compiler] Remove `Lconstruct` from lambda code.Maxime Dénès
This is a step towards unifying the higher level ILs of the native and bytecode compilers. See https://github.com/coq/coq/projects/17
2019-04-14Merge PR #9957: Add missing build dependency in `coq.opam`Emilio Jesus Gallego Arias
Reviewed-by: ejgallego
2019-04-14Fix coq/coq#9956Erik Martin-Dorel
2019-04-12Merge PR #9949: [stm] Report correct ids on some errors where it was dummy.Enrico Tassi
Reviewed-by: gares
2019-04-11[stm] Report correct ids on some errors where it was dummy.Shachar Itzhaky
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-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-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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 18:39:29 +0000