aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
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-05Merge PR #8871: [library] Move Nametab/Lib specific-names to NametabHugo Herbelin
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 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.
2018-11-02Merge PR #8895: gitignore test-suite/misc/poly-capture-global-univs/src/evil.mlPierre-Marie Pédrot
2018-11-02Merge PR #8809: [dev doc] Update proof engine docs, fixes #6640Pierre-Marie Pédrot
2018-11-02Expose Typing.judge_of_applyGaëtan Gilbert
This can be useful to avoid [Typing.type_of (App (f,args))] when working with universe polymorphism.
2018-11-02Remove ml4 from Coq's make build systemGaëtan Gilbert
2018-11-02Select OS specific coqide code with cp.Gaëtan Gilbert
2018-11-02Add dev/changes about attribute syntax in mlgGaëtan Gilbert
2018-11-02Add overlays (command driven attributes)Gaëtan Gilbert
2018-11-02coqpp VERNAC EXTEND uses #[ att = attribute; ] syntaxGaëtan Gilbert
I think for instance the new code in this diff is cleaner and more systematic: ~~~diff VERNAC COMMAND EXTEND VernacDeclareTacticDefinition -| [ "Ltac" ne_ltac_tacdef_body_list_sep(l, "with") ] => { +| #[ deprecation; locality; ] [ "Ltac" ne_ltac_tacdef_body_list_sep(l, "with") ] => { VtSideff (List.map (function | TacticDefinition ({CAst.v=r},_) -> r | TacticRedefinition (qid,_) -> qualid_basename qid) l), VtLater } -> { - let deprecation, locality = Attributes.(parse Notations.(deprecation ++ locality) atts) in Tacentries.register_ltac (Locality.make_module_locality locality) ?deprecation l; } END ~~~
2018-11-02Universe Polymorphism is a normal attribute modulo the stm (no Flags)Gaëtan Gilbert
2018-11-02Per command attribute parsing for core commandsGaëtan Gilbert
2018-11-02Add comment in stm to unsupport attributes for special commandsGaëtan Gilbert
2018-11-02Load doesn't support attributesGaëtan Gilbert
2018-11-02Simplify use of polymorphism/program globals in attributesGaëtan Gilbert
2018-11-02Remove is_universe_polymorphism from printingGaëtan Gilbert
2018-11-02Remove incorrect is_universe_polymorphism from modinternGaëtan Gilbert
2018-11-02rewrite: attributes handle is_univ_poly, is_program_modeGaëtan Gilbert
2018-11-02Remove is_universe_polymorphism in funindGaëtan Gilbert
Funind doesn't support polymorphism.
2018-11-02Remove is_universe_polymorphic in indschemesGaëtan Gilbert
2018-11-02Remove evdref style in build_combined_schemeGaëtan Gilbert
2018-11-02Generalize attributes further to get a monad (mostly for [map])Gaëtan Gilbert
Having [map] means we can structure attributes when combining them, eg get an attribute for [type universe_data = { poly : bool option; template : bool option }] from 2 [bool option] attributes. Using the previous representation we would have had to provide the inverse function [universe_data -> bool option * bool option] as well. An alternate way to get (++) is let (++) (x:'a t) (y:'b t) : ('a*'b) t = x >>= fun xv -> y >>= fun yv -> return (xv,yv) Not sure if that would be cleaner.
2018-11-02Make attributes more general to make defining #[universes(...)] easyGaëtan Gilbert
2018-11-02Command driven attributes.Gaëtan Gilbert
Commands need to request the attributes they use, with the API encouraging them to error on unsupported attributes.
2018-11-02Remove pointless optional arguments to mk_attsGaëtan Gilbert
2018-11-02{Vernacentries -> Attributes}.attributes_of_flagsGaëtan Gilbert
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 09:43:29 +0000