aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2018-11-06Merge PR #8912: [dune] [coqide] Use copy action instead of (run cp ...)Théo Zimmermann
2018-11-06Merge PR #8903: [dune] Add to vo rules explicit location of coqlib in boot mode.Théo Zimmermann
2018-11-06Merge PR #8884: Improve rendering of the credits.Théo Zimmermann
2018-11-06Merge PR #8556: [ssr] use tclDISPATCH for IPatDispatch (fix #8544)Maxime Dénès
2018-11-06Merge PR #8915: More cleanup of vendored camlp5Emilio Jesus Gallego Arias
2018-11-06[travis] Add Travis File.Emilio Jesus Gallego Arias
We only test dev for master.
2018-11-06Removing dead code in Plexing.Pierre-Marie Pédrot
It was full with utility functions and wrappers that are unused in the Coq codebase.
2018-11-06Remove the non-functorial interface of camlp5 grammars.Pierre-Marie Pédrot
2018-11-06Add overlay for EquationsMatthieu Sozeau
2018-11-06[program] extend obligation to give back a mapping from obligations toMatthieu Sozeau
terms This is necessary for programs like Equations that call add_definition and want to later update in their hook some separate datastructures which refer to the obligations that are defined by Program. We give back a map from obligation name to a constr defined in the program's universe state which the hook returns as well. (Obligation names also correspond to undefined evars in the original terms through Obligations.eterm_obligations). Using this, I can avoid ucontext_of_aucontext in Equations, allowing PR #8601 to go through.
2018-11-06Improve rendering of the credits.Guillaume Melquiond
This mostly fixes text that was italicized instead of teletyped. When possible, tactic names have been made to point to their documentation. Also, the date of the 8.9 release has been proactively changed to November.
2018-11-06Merge PR #8907: Cleanup camlp5 dead codeEmilio Jesus Gallego Arias
2018-11-06[dune] [coqide] Use copy action instead of (run cp ...)Emilio Jesus Gallego Arias
This is a bit more portable.
2018-11-05Remove patches of dead code in Gramlib.Pierre-Marie Pédrot
2018-11-05Remove the Scut constructor from Gramlib.Pierre-Marie Pédrot
This constructor only makes sense in the backtracking mode, that has been removed from our vendored version of camlp5.
2018-11-05Remove the Sflag constructor from Gramlib.Pierre-Marie Pédrot
It is just a wrapper around Sopt. I do not really understand why it is hardwired in the entry AST.
2018-11-05Remove the Sfacto constructor from Gramlib.Pierre-Marie Pédrot
Used by rule factorisation in theory, but appears to be unused in Coq.
2018-11-05Remove the Svala constructor from Gramlib.Pierre-Marie Pédrot
It is only used in strict mode, which makes no sense for Coq grammar.
2018-11-05Remove Smeta constructor in Gramlib.Pierre-Marie Pédrot
This constructor was only used by meta-level macros that are not used and serve no purpose in the grammar engine.
2018-11-05[dune] Add to vo rules explicit location of coqlib in boot mode.Emilio Jesus Gallego Arias
When `-coqlib $PATH` is absent, Coq will try to locate coqlib using a heuristic based on the name of the executable. The code in `envars.ml` basically does: ```ocaml Filename.(dirname CUnix.(canonical_path_name (dirname Sys.executable_name))) ``` which doesn't seem to work very well on Windows and OSX when `coqtop` is a symlink. Instead, we now pass the right `-coqlib` to coqtop from `coq_dune`. Maybe fixes #8862.
2018-11-05Merge PR #8899: Remove the deprecated Token module and port the ↵Emilio Jesus Gallego Arias
corresponding code.
2018-11-05Merge PR #8815: NArith: add lemmas about numbers and vectorsHugo Herbelin
2018-11-05Port to coqpp.Pierre-Marie Pédrot
2018-11-05Merge PR #8871: [library] Move Nametab/Lib specific-names to NametabHugo Herbelin
2018-11-05Merge pull request #12 from SkySkimmer/command-attsYves Bertot
Fix for coq/coq#8515 (command driven attributes)
2018-11-05[Goptions] More detailed error messagesVincent Laporte
2018-11-05Merge pull request coq/ltac2#75 from SkySkimmer/command-attsPierre-Marie Pédrot
Fix for coq/coq#8515 (command driven attributes)
2018-11-05Merge PR #8515: Command driven attributesPierre-Marie Pédrot
2018-11-05Merge PR #8870: Pass native and VM flags to the kernel through environmentPierre-Marie Pédrot
2018-11-05Merge PR #7952: Fix an algorithmic issue in the vernac guardedness checker.Gaëtan Gilbert
2018-11-05Merge PR #8896: Expose Typing.judge_of_applyPierre-Marie Pédrot
2018-11-05Merge PR #8866: Check universe instances in TypingPierre-Marie Pédrot
2018-11-05Merge PR #8824: Do not check convertibility of pattern types in the kernelMaxime Dénès
2018-11-05Merge PR #8874: Fix #8873: coqchk on inductive with letin parameterPierre-Marie Pédrot
2018-11-05Merge PR #8882: Fix #8881: validate fails to use inductive equivalence in ↵Pierre-Marie Pédrot
case_info
2018-11-05Merge PR #8857: [library] Better sizing for libobject hashtbl.Pierre-Marie Pédrot
2018-11-05Merge PR #8766: [nametab] [api] Provide basic support for efficient completion.Pierre-Marie Pédrot
2018-11-05Merge PR #8836: [default.nix] Add coq-version and setupHook.Vincent Laporte
2018-11-05Pass native and VM flags to the kernel through environmentMaxime Dénès
The kernel no longer has to read the configure flag, its value can now be overriden by a coqtop/coqc argument, and more generally is easier to set from a toplevel (such as the checker). We also add a `-bytecode-compiler` flag. Fixes #4607
2018-11-05Merge PR #8842: Towards seeing Global purely as a wrapper on top of kernel ↵Maxime Dénès
functions
2018-11-05Merge PR #8843: Remove coqide ml4Pierre-Marie Pédrot
2018-11-05[default.nix] Update pinned nixpkgs.Théo Zimmermann
2018-11-05[default.nix] Add coq-version, meta.platform and setupHook.Théo Zimmermann
Closes #8227 by solving remaining differences. Sets dontFilter in anticipation of NixOS/nixpkgs#49456.
2018-11-04Remove the deprecated Token module and port the corresponding code.Pierre-Marie Pédrot
2018-11-03Merge PR #8877: Fix #8876: expected number of arguments for cumulative ↵Pierre-Marie Pédrot
constructors
2018-11-03Merge PR #8745: Fixes #3468: making tactic-in-term sensitive to ↵Pierre-Marie Pédrot
interpretation scopes
2018-11-03Merge pull request coq/ltac2#82 from SkySkimmer/split-tacticsPierre-Marie Pédrot
Adapt to coq/coq#8844 (move abstract out of tactics.ml)
2018-11-03Merge PR #8844: Move abstract out of tactics.mlPierre-Marie Pédrot
2018-11-03Merge PR #8852: Use the obligation evar flagPierre-Marie Pédrot
2018-11-02Merge PR #8834: [error printing] Fix improper grounding of open terms in ↵Hugo Herbelin
printing.
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-25 14:26:16 +0000