aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2019-04-16Command-line setters for optionsGaëtan Gilbert
TODO coqproject handling (for now it can be done through -arg I guess)
2019-04-16[CI/Azure/macOS] Set MACOSX_DEPLOYMENT_TARGET to 10.12Vincent Laporte
2019-04-16[CI/Azure/macOS] Install Coq into an artifactVincent Laporte
2019-04-15Update critical-bugsPierre Roux
2019-04-15[vm] Protect accu and coq_envPierre Roux
Protect accu and coq_env against GC calls in the VM when calling primitive integer functions on 32 bits architecture.
2019-04-15[native compiler] Encoding of constructors based on tagsMaxime Dénès
This serves two purposes: 1. It makes the native compiler use the same encoding and lambda-representation as the bytecode compiler 2. It avoid relying on fragile invariants relating tags and constructor indices. For example, previously, the mapping from indices to tags had to be increasing.
2019-04-15[native compiler] Remove unused universe argument in LmakeblockMaxime Dénès
2019-04-15[native compiler] Distinguish constant constructors in lambda codeMaxime Dénès
2019-04-15[CI/Azure/macOS] Build CoqIDEVincent Laporte
2019-04-15[CoqIDE] Fix build system for macOSVincent Laporte
2019-04-15[CI] Print test-suite log on failure (macOS/Azure)Vincent Laporte
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-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).
generated by cgit v1.2.3 (git 2.25.1) at 2026-07-26 19:54:47 +0000