diff options
72 files changed, 529 insertions, 489 deletions
diff --git a/.gitignore b/.gitignore index f741135211..538124b8e5 100644 --- a/.gitignore +++ b/.gitignore @@ -68,6 +68,7 @@ time-of-build-after.log .csdp.cache test-suite/.lia.cache test-suite/.nra.cache +test-suite/.nia.cache test-suite/trace test-suite/misc/universes/all_stdlib.v test-suite/misc/universes/universes.txt @@ -165,8 +166,6 @@ checker/esubst.mli user-contrib .*.sw* .#* -test-suite/.lia.cache -test-suite/.nra.cache plugins/ssr/ssrparser.ml plugins/ssr/ssrvernac.ml diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 1669145d9b..01931fd7ef 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -9,7 +9,7 @@ stages: variables: # Format: $IMAGE-V$DATE [Cache is not used as of today but kept here # for reference] - CACHEKEY: "bionic_coq-V2018-10-04-V1" + CACHEKEY: "bionic_coq-V2018-10-23-V1" IMAGE: "$CI_REGISTRY_IMAGE:$CACHEKEY" # By default, jobs run in the base switch; override to select another switch OPAM_SWITCH: "base" diff --git a/CHANGES.md b/CHANGES.md index 865e1eeb95..ada68f97d5 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -241,6 +241,8 @@ Standard Library - There are now conversions between `string` and `positive`, `Z`, `nat`, and `N` in binary, octal, and hex. +- Added `ByteVector` type that can convert to and from [string]. + Display diffs between proof steps - `coqtop` and `coqide` can now highlight the differences between proof steps diff --git a/checker/closure.ml b/checker/closure.ml index 5706011607..138499b0e6 100644 --- a/checker/closure.ml +++ b/checker/closure.ml @@ -121,9 +121,6 @@ let betaiotazeta = mkflags [fBETA;fIOTA;fZETA] * abstractions, storing a representation (of type 'a) of the body of * this constant or abstraction. * * i_tab is the cache table of the results - * * i_repr is the function to get the representation from the current - * state of the cache and the body of the constant. The result - * is stored in the table. * * i_rels = (4,[(1,c);(3,d)]) means there are 4 free rel variables * and only those with index 1 and 3 have bodies which are c and d resp. * @@ -156,33 +153,6 @@ end module KeyTable = Hashtbl.Make(KeyHash) -type 'a infos = { - i_flags : reds; - i_repr : 'a infos -> constr -> 'a; - i_env : env; - i_rels : int * (int * constr) list; - i_tab : 'a KeyTable.t } - -let ref_value_cache info ref = - try - Some (KeyTable.find info.i_tab ref) - with Not_found -> - try - let body = - match ref with - | RelKey n -> - let (s,l) = info.i_rels in lift n (Int.List.assoc (s-n) l) - | VarKey id -> raise Not_found - | ConstKey cst -> constant_value info.i_env cst - in - let v = info.i_repr info body in - KeyTable.add info.i_tab ref v; - Some v - with - | Not_found (* List.assoc *) - | NotEvaluableConst _ (* Const *) - -> None - let defined_rels flags env = (* if red_local_const (snd flags) then*) fold_rel_context @@ -193,16 +163,6 @@ let defined_rels flags env = (rel_context env) ~init:(0,[]) (* else (0,[])*) -let mind_equiv_infos info = mind_equiv info.i_env - -let create mk_cl flgs env = - { i_flags = flgs; - i_repr = mk_cl; - i_env = env; - i_rels = defined_rels flgs env; - i_tab = KeyTable.create 17 } - - (**********************************************************************) (* Lazy reduction: the one used in kernel operations *) @@ -255,6 +215,12 @@ and fterm = | FCLOS of constr * fconstr subs | FLOCKED +type clos_infos = { + i_flags : reds; + i_env : env; + i_rels : int * (int * constr) list; + i_tab : fconstr KeyTable.t } + let fterm_of v = v.term let set_norm v = v.norm <- Norm @@ -372,6 +338,30 @@ let mk_clos e t = let mk_clos_vect env v = Array.map (mk_clos env) v +let inject = mk_clos (subs_id 0) + +let ref_value_cache info ref = + try + Some (KeyTable.find info.i_tab ref) + with Not_found -> + try + let body = + match ref with + | RelKey n -> + let (s,l) = info.i_rels in lift n (Int.List.assoc (s-n) l) + | VarKey id -> raise Not_found + | ConstKey cst -> constant_value info.i_env cst + in + let v = inject body in + KeyTable.add info.i_tab ref v; + Some v + with + | Not_found (* List.assoc *) + | NotEvaluableConst _ (* Const *) + -> None + +let mind_equiv_infos info = mind_equiv info.i_env + (* Translate the head constructor of t from constr to fconstr. This function is parameterized by the function to apply on the direct subterms. @@ -783,21 +773,19 @@ let kh info v stk = fapp_stack(kni info v stk) let whd_val info v = with_stats (lazy (term_of_fconstr (kh info v []))) -let inject = mk_clos (subs_id 0) - let whd_stack infos m stk = let k = kni infos m stk in let _ = fapp_stack k in (* to unlock Zupdates! *) k -(* cache of constants: the body is computed only when needed. *) -type clos_infos = fconstr infos - let infos_env x = x.i_env let infos_flags x = x.i_flags let oracle_of_infos x = x.i_env.env_conv_oracle let create_clos_infos flgs env = - create (fun _ -> inject) flgs env + { i_flags = flgs; + i_env = env; + i_rels = defined_rels flgs env; + i_tab = KeyTable.create 17 } let unfold_reference = ref_value_cache diff --git a/checker/closure.mli b/checker/closure.mli index cec785699d..4c6643754b 100644 --- a/checker/closure.mli +++ b/checker/closure.mli @@ -61,10 +61,6 @@ val betadeltaiotanolet : reds type table_key = Constant.t puniverses tableKey -type 'a infos -val ref_value_cache: 'a infos -> table_key -> 'a option -val create: ('a infos -> constr -> 'a) -> reds -> env -> 'a infos - (************************************************************************) (*s Lazy reduction. *) diff --git a/checker/reduction.ml b/checker/reduction.ml index d36c0ef2c9..58a3f4e410 100644 --- a/checker/reduction.ml +++ b/checker/reduction.ml @@ -280,17 +280,26 @@ let get_strategy { var_opacity; cst_opacity } = function with Not_found -> default_level) | RelKey _ -> Expand +let dep_order l2r k1 k2 = match k1, k2 with +| RelKey _, RelKey _ -> l2r +| RelKey _, (VarKey _ | ConstKey _) -> true +| VarKey _, RelKey _ -> false +| VarKey _, VarKey _ -> l2r +| VarKey _, ConstKey _ -> true +| ConstKey _, (RelKey _ | VarKey _) -> false +| ConstKey _, ConstKey _ -> l2r + let oracle_order infos l2r k1 k2 = let o = Closure.oracle_of_infos infos in match get_strategy o k1, get_strategy o k2 with - | Expand, Expand -> l2r + | Expand, Expand -> dep_order l2r k1 k2 | Expand, (Opaque | Level _) -> true | (Opaque | Level _), Expand -> false - | Opaque, Opaque -> l2r + | Opaque, Opaque -> dep_order l2r k1 k2 | Level _, Opaque -> true | Opaque, Level _ -> false | Level n1, Level n2 -> - if Int.equal n1 n2 then l2r + if Int.equal n1 n2 then dep_order l2r k1 k2 else n1 < n2 let eq_table_key univ = @@ -1,18 +1,28 @@ -opam-version: "1.2" +synopsis: "The Coq Proof Assistant" +description: """ +Coq is a formal proof management system. It provides +a formal language to write mathematical definitions, executable +algorithms and theorems together with an environment for +semi-interactive development of machine-checked proofs. Typical +applications include the certification of properties of programming +languages (e.g. the CompCert compiler certification project, or the +Bedrock verified low-level programming library), the formalization of +mathematics (e.g. the full formalization of the Feit-Thompson theorem +or homotopy type theory) and teaching. +""" +opam-version: "2.0" maintainer: "The Coq development team <coqdev@inria.fr>" authors: "The Coq development team, INRIA, CNRS, and contributors." homepage: "https://coq.inria.fr/" bug-reports: "https://github.com/coq/coq/issues" -dev-repo: "https://github.com/coq/coq.git" +dev-repo: "git+https://github.com/coq/coq.git" license: "LGPL-2.1" -available: [ ocaml-version >= "4.05.0" ] - depends: [ - "dune" { build & >= "1.2.0" } - "ocamlfind" { build } + "ocaml" { >= "4.05.0" } + "dune" { build & >= "1.4.0" } "num" - "camlp5" { >= "7.03" } + "camlp5" { >= "7.03" } ] build-env: [ diff --git a/coqide-server.opam b/coqide-server.opam index 546ce75dbd..ed6f3d98d8 100644 --- a/coqide-server.opam +++ b/coqide-server.opam @@ -1,15 +1,25 @@ -opam-version: "1.2" +synopsis: "The Coq Proof Assistant" +description: """ +Coq is a formal proof management system. It provides +a formal language to write mathematical definitions, executable +algorithms and theorems together with an environment for +semi-interactive development of machine-checked proofs. + +This package provides the `coqidetop` language server, an +implementation of Coq's [XML protocol](https://github.com/coq/coq/blob/master/dev/doc/xml-protocol.md) +which allows clients, such as CoqIDE, to interact with Coq in a +structured way. +""" +opam-version: "2.0" maintainer: "The Coq development team <coqdev@inria.fr>" authors: "The Coq development team, INRIA, CNRS, and contributors." homepage: "https://coq.inria.fr/" bug-reports: "https://github.com/coq/coq/issues" -dev-repo: "https://github.com/coq/coq.git" +dev-repo: "git+https://github.com/coq/coq.git" license: "LGPL-2.1" -available: [ocaml-version >= "4.05.0"] - depends: [ - "dune" { build & >= "1.2.0" } + "dune" { build & >= "1.4.0" } "coq" ] diff --git a/coqide.opam b/coqide.opam index 17fb5dbbe2..314943a881 100644 --- a/coqide.opam +++ b/coqide.opam @@ -1,16 +1,23 @@ -opam-version: "1.2" +synopsis: "The Coq Proof Assistant" +description: """ +Coq is a formal proof management system. It provides +a formal language to write mathematical definitions, executable +algorithms and theorems together with an environment for +semi-interactive development of machine-checked proofs. + +This package provides the CoqIDE, a graphical user interface for the +development of interactive proofs. +""" +opam-version: "2.0" maintainer: "The Coq development team <coqdev@inria.fr>" authors: "The Coq development team, INRIA, CNRS, and contributors." homepage: "https://coq.inria.fr/" bug-reports: "https://github.com/coq/coq/issues" -dev-repo: "https://github.com/coq/coq.git" +dev-repo: "git+https://github.com/coq/coq.git" license: "LGPL-2.1" -available: [ocaml-version >= "4.05.0"] - depends: [ - "dune" { build & >= "1.2.0" } - "coq" + "dune" { build & >= "1.4.0" } "coqide-server" "conf-gtksourceview" "lablgtk" { >= "2.18.5" } diff --git a/dev/ci/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile index f257c62dd3..098c950b32 100644 --- a/dev/ci/docker/bionic_coq/Dockerfile +++ b/dev/ci/docker/bionic_coq/Dockerfile @@ -1,4 +1,4 @@ -# CACHEKEY: "bionic_coq-V2018-10-04-V2" +# CACHEKEY: "bionic_coq-V2018-10-23-V1" # ^^ Update when modifying this file. FROM ubuntu:bionic @@ -37,7 +37,7 @@ ENV COMPILER="4.05.0" # Common OPAM packages. # `num` does not have a version number as the right version to install varies # with the compiler version. -ENV BASE_OPAM="num ocamlfind.1.8.0 dune.1.2.1 ounit.2.0.8 odoc.1.2.0" \ +ENV BASE_OPAM="num ocamlfind.1.8.0 dune.1.4.0 ounit.2.0.8 odoc.1.3.0" \ CI_OPAM="menhir.20180530 elpi.1.1.0 ocamlgraph.1.8.8" # BASE switch; CI_OPAM contains Coq's CI dependencies. @@ -56,7 +56,7 @@ RUN opam switch create "${COMPILER}+32bit" && eval $(opam env) && \ ENV COMPILER_EDGE="4.07.0" \ CAMLP5_VER_EDGE="7.06" \ COQIDE_OPAM_EDGE="lablgtk.2.18.6 conf-gtksourceview.2" \ - BASE_OPAM_EDGE="dune-release.0.3.0" + BASE_OPAM_EDGE="dune-release.1.1.0" RUN opam switch create $COMPILER_EDGE && eval $(opam env) && \ opam install $BASE_OPAM $BASE_OPAM_EDGE camlp5.$CAMLP5_VER_EDGE $COQIDE_OPAM_EDGE diff --git a/dev/dune-workspace.all b/dev/dune-workspace.all index 93b807d5e3..f45f6de529 100644 --- a/dev/dune-workspace.all +++ b/dev/dune-workspace.all @@ -1,4 +1,4 @@ -(lang dune 1.2) +(lang dune 1.4) ; Add custom flags here. Default developer profile is `dev` (context (opam (switch 4.05.0))) diff --git a/doc/sphinx/credits.rst b/doc/sphinx/credits.rst index ffdc4f3ec6..57f1174d59 100644 --- a/doc/sphinx/credits.rst +++ b/doc/sphinx/credits.rst @@ -120,7 +120,7 @@ G. Dowek, allowed hierarchical developments of mathematical theories. This high-level language was called the *Mathematical Vernacular*. Furthermore, an interactive *Theorem Prover* permitted the incremental construction of proof trees in a top-down manner, subgoaling recursively -and backtracking from dead-alleys. The theorem prover executed tactics +and backtracking from dead-ends. The theorem prover executed tactics written in CAML, in the LCF fashion. A basic set of tactics was predefined, which the user could extend by his own specific tactics. This system (Version 4.10) was released in 1989. Then, the system was diff --git a/doc/sphinx/language/cic.rst b/doc/sphinx/language/cic.rst index 381f8bb661..835d6dcaa6 100644 --- a/doc/sphinx/language/cic.rst +++ b/doc/sphinx/language/cic.rst @@ -533,10 +533,10 @@ Convertibility Let us write :math:`E[Γ] ⊢ t \triangleright u` for the contextual closure of the relation :math:`t` reduces to :math:`u` in the global environment :math:`E` and local context :math:`Γ` with one of the previous -reductions β, ι, δ or ζ. +reductions β, δ, ι or ζ. We say that two terms :math:`t_1` and :math:`t_2` are -*βιδζη-convertible*, or simply *convertible*, or *equivalent*, in the +*βδιζη-convertible*, or simply *convertible*, or *equivalent*, in the global environment :math:`E` and local context :math:`Γ` iff there exist terms :math:`u_1` and :math:`u_2` such that :math:`E[Γ] ⊢ t_1 \triangleright … \triangleright u_1` and :math:`E[Γ] ⊢ t_2 \triangleright … \triangleright u_2` and either :math:`u_1` and diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst index c802f44ac1..741f9fe5b0 100644 --- a/doc/sphinx/proof-engine/proof-handling.rst +++ b/doc/sphinx/proof-engine/proof-handling.rst @@ -144,8 +144,9 @@ list of assertion commands is given in :ref:`Assertions`. The command the proof is a subset of the declared one. The set of declared variables is closed under type dependency. For - example if ``T`` is variable and a is a variable of type ``T``, the commands - ``Proof using a`` and ``Proof using T a`` are actually equivalent. + example, if ``T`` is a variable and ``a`` is a variable of type + ``T``, then the commands ``Proof using a`` and ``Proof using T a`` + are equivalent. .. cmdv:: Proof using {+ @ident } with @tactic diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst index 52609546d5..3ca0ffe678 100644 --- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst +++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst @@ -916,11 +916,8 @@ but also folds ``x`` in the goal. .. coqtop:: reset From Coq Require Import ssreflect. - Set Implicit Arguments. - Unset Strict Implicit. - Unset Printing Implicit Defensive. - .. coqtop:: all undo + .. coqtop:: all Lemma test x t (Hx : x = 3) : x + t = 4. set z := 3 in Hx. @@ -929,6 +926,10 @@ If the localization also mentions the goal, then the result is the following one .. example:: + .. coqtop:: reset + + From Coq Require Import ssreflect. + .. coqtop:: all Lemma test x t (Hx : x = 3) : x + t = 4. @@ -2485,8 +2486,7 @@ destruction of existential assumptions like in the tactic: .. coqtop:: all Lemma test : True. - have [x Px]: exists x : nat, x > 0. - Focus 2. + have [x Px]: exists x : nat, x > 0; last first. An alternative use of the ``have`` tactic is to provide the explicit proof term for the intermediate lemma, using tactics of the form: @@ -2564,8 +2564,7 @@ copying the goal itself. .. coqtop:: all Lemma test : True. - have suff H : 2 + 2 = 3. - Focus 2. + have suff H : 2 + 2 = 3; last first. Note that H is introduced in the second goal. @@ -2852,8 +2851,7 @@ pattern will be used to process its instance. .. coqtop:: all Lemma simple n (ngt0 : 0 < n ) : P n. - gen have ltnV, /andP[nge0 neq0] : n ngt0 / (0 <= n) && (n != 0). - Focus 2. + gen have ltnV, /andP[nge0 neq0] : n ngt0 / (0 <= n) && (n != 0); last first. .. _advanced_generalization_ssr: @@ -3556,6 +3554,7 @@ corresponding new goals will be generated. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. + Set Warnings "-notation-overridden". .. coqtop:: all @@ -3756,9 +3755,10 @@ which the function is supplied: :name: congr This tactic: -+ checks that the goal is a Leibniz equality -+ matches both sides of this equality with “term applied to some arguments”, inferring the right number of arguments from the goal and the type of term. This may expand some definitions or fixpoints. -+ generates the subgoals corresponding to pairwise equalities of the arguments present in the goal. + + + checks that the goal is a Leibniz equality; + + matches both sides of this equality with “term applied to some arguments”, inferring the right number of arguments from the goal and the type of term. This may expand some definitions or fixpoints; + + generates the subgoals corresponding to pairwise equalities of the arguments present in the goal. The goal can be a non dependent product ``P -> Q``. In that case, the system asserts the equation ``P = Q``, uses it to solve the goal, and @@ -4918,7 +4918,7 @@ which produces the converse implication. In both cases, the two first Prop arguments are implicit. If ``term`` is an instance of the ``reflect`` predicate, then ``A`` will be one -of the defined view hints for the ``reflec``t predicate, which are by +of the defined view hints for the ``reflect`` predicate, which are by default the ones present in the file ``ssrbool.v``. These hints are not only used for choosing the appropriate direction of the translation, but they also allow complex transformation, involving negations. @@ -4933,9 +4933,9 @@ but they also allow complex transformation, involving negations. Unset Printing Implicit Defensive. Section Test. - .. coqtop:: in + .. coqtop:: all - Lemma introN : forall (P : Prop) (b : bool), reflect P b -> ~ P -> ~~b. + Check introN. .. coqtop:: all @@ -4945,12 +4945,11 @@ but they also allow complex transformation, involving negations. In fact this last script does not exactly use the hint ``introN``, but the more general hint: - .. coqtop:: in + .. coqtop:: all - Lemma introNTF : forall (P : Prop) (b c : bool), - reflect P b -> (if c then ~ P else P) -> ~~ b = c. + Check introNTF. - The lemma ` `introN`` is an instantiation of introNF using c := true. + The lemma ``introN`` is an instantiation of ``introNF`` using ``c := true``. Note that views, being part of :token:`i_pattern`, can be used to interpret assertions too. For example the following script asserts ``a && b`` but diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template index 4cbf75b715..e8f6decfbf 100644 --- a/doc/stdlib/index-list.html.template +++ b/doc/stdlib/index-list.html.template @@ -502,6 +502,7 @@ through the <tt>Require Import</tt> command.</p> theories/Strings/BinaryString.v theories/Strings/HexString.v theories/Strings/OctalString.v + theories/Strings/ByteVector.v </dd> <dt> <b>Reals</b>: @@ -38,4 +38,5 @@ ; Use summary.log as the target (alias (name runtest) + (package coqide-server) (deps test-suite/summary.log)) diff --git a/dune-project b/dune-project index 607e5a68a5..85238c70c5 100644 --- a/dune-project +++ b/dune-project @@ -1,3 +1,3 @@ -(lang dune 1.2) +(lang dune 1.4) (name coq) diff --git a/engine/namegen.ml b/engine/namegen.ml index 7ce759a3fb..db72dc8ec3 100644 --- a/engine/namegen.ml +++ b/engine/namegen.ml @@ -21,7 +21,6 @@ open Constr open Environ open EConstr open Vars -open Nametab open Nameops open Libnames open Globnames @@ -82,14 +81,14 @@ let is_imported_ref = function let is_global id = try - let ref = locate (qualid_of_ident id) in + let ref = Nametab.locate (qualid_of_ident id) in not (is_imported_ref ref) with Not_found -> false let is_constructor id = try - match locate (qualid_of_ident id) with + match Nametab.locate (qualid_of_ident id) with | ConstructRef _ -> true | _ -> false with Not_found -> @@ -116,7 +115,7 @@ let head_name sigma c = (* Find the head constant of a constr if any *) | Cast (c,_,_) | App (c,_) -> hdrec c | Proj (kn,_) -> Some (Label.to_id (Constant.label (Projection.constant kn))) | Const _ | Ind _ | Construct _ | Var _ as c -> - Some (basename_of_global (global_of_constr c)) + Some (Nametab.basename_of_global (global_of_constr c)) | Fix ((_,i),(lna,_,_)) | CoFix (i,(lna,_,_)) -> Some (match lna.(i) with Name id -> id | _ -> assert false) | Sort _ | Rel _ | Meta _|Evar _|Case (_, _, _, _) -> None @@ -148,8 +147,8 @@ let hdchar env sigma c = | Cast (c,_,_) | App (c,_) -> hdrec k c | Proj (kn,_) -> lowercase_first_char (Label.to_id (Constant.label (Projection.constant kn))) | Const (kn,_) -> lowercase_first_char (Label.to_id (Constant.label kn)) - | Ind (x,_) -> (try lowercase_first_char (basename_of_global (IndRef x)) with Not_found when !Flags.in_debugger -> "zz") - | Construct (x,_) -> (try lowercase_first_char (basename_of_global (ConstructRef x)) with Not_found when !Flags.in_debugger -> "zz") + | Ind (x,_) -> (try lowercase_first_char (Nametab.basename_of_global (IndRef x)) with Not_found when !Flags.in_debugger -> "zz") + | Construct (x,_) -> (try lowercase_first_char (Nametab.basename_of_global (ConstructRef x)) with Not_found when !Flags.in_debugger -> "zz") | Var id -> lowercase_first_char id | Sort s -> sort_hdchar (ESorts.kind sigma s) | Rel n -> @@ -267,7 +266,7 @@ let visible_ids sigma (nenv, c) = begin try let gseen = GlobRef.Set_env.add g gseen in - let short = shortest_qualid_of_global Id.Set.empty g in + let short = Nametab.shortest_qualid_of_global Id.Set.empty g in let dir, id = repr_qualid short in let ids = if DirPath.is_empty dir then Id.Set.add id ids else ids in accu := (gseen, vseen, ids) diff --git a/engine/termops.ml b/engine/termops.ml index ee0c3d210e..e1f5fb0d7f 100644 --- a/engine/termops.ml +++ b/engine/termops.ml @@ -816,26 +816,11 @@ let map_constr_with_full_binders_user_view sigma g f = each binder traversal; it is not recursive *) let fold_constr_with_full_binders sigma g f n acc c = - let open RelDecl in - match EConstr.kind sigma c with - | (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _ - | Construct _) -> acc - | Cast (c,_, t) -> f n (f n acc c) t - | Prod (na,t,c) -> f (g (LocalAssum (na, t)) n) (f n acc t) c - | Lambda (na,t,c) -> f (g (LocalAssum (na, t)) n) (f n acc t) c - | LetIn (na,b,t,c) -> f (g (LocalDef (na, b, t)) n) (f n (f n acc b) t) c - | App (c,l) -> Array.fold_left (f n) (f n acc c) l - | Proj (p,c) -> f n acc c - | Evar (_,l) -> Array.fold_left (f n) acc l - | Case (_,p,c,bl) -> Array.fold_left (f n) (f n (f n acc p) c) bl - | Fix (_,(lna,tl,bl)) -> - let n' = CArray.fold_left2 (fun c n t -> g (LocalAssum (n, t)) c) n lna tl in - let fd = Array.map2 (fun t b -> (t,b)) tl bl in - Array.fold_left (fun acc (t,b) -> f n' (f n acc t) b) acc fd - | CoFix (_,(lna,tl,bl)) -> - let n' = CArray.fold_left2 (fun c n t -> g (LocalAssum (n, t)) c) n lna tl in - let fd = Array.map2 (fun t b -> (t,b)) tl bl in - Array.fold_left (fun acc (t,b) -> f n' (f n acc t) b) acc fd + let open EConstr in + let f l acc c = f l acc (of_constr c) in + let g d l = g (of_rel_decl d) l in + let c = Unsafe.to_constr (whd_evar sigma c) in + Constr.fold_with_full_binders g f n acc c let fold_constr_with_binders sigma g f n acc c = fold_constr_with_full_binders sigma (fun _ x -> g x) f n acc c diff --git a/engine/univGen.ml b/engine/univGen.ml index 23ab30eb75..130aa06f53 100644 --- a/engine/univGen.ml +++ b/engine/univGen.ml @@ -77,17 +77,14 @@ let fresh_global_instance ?loc ?names env gr = let u, ctx = fresh_global_instance ?loc ?names env gr in mkRef (gr, u), ctx -let constr_of_global gr = - let c, ctx = fresh_global_instance (Global.env ()) gr in - if not (Univ.ContextSet.is_empty ctx) then - if Univ.LSet.is_empty (Univ.ContextSet.levels ctx) then - (* Should be an error as we might forget constraints, allow for now - to make firstorder work with "using" clauses *) - c - else CErrors.user_err ~hdr:"constr_of_global" - Pp.(str "globalization of polymorphic reference " ++ Nametab.pr_global_env Id.Set.empty gr ++ - str " would forget universes.") - else c +let constr_of_monomorphic_global gr = + if not (Global.is_polymorphic gr) then + fst (fresh_global_instance (Global.env ()) gr) + else CErrors.user_err ~hdr:"constr_of_global" + Pp.(str "globalization of polymorphic reference " ++ Nametab.pr_global_env Id.Set.empty gr ++ + str " would forget universes.") + +let constr_of_global gr = constr_of_monomorphic_global gr let constr_of_global_univ = mkRef diff --git a/engine/univGen.mli b/engine/univGen.mli index c2e9d0c696..42756701dc 100644 --- a/engine/univGen.mli +++ b/engine/univGen.mli @@ -74,11 +74,16 @@ val extend_context : 'a in_universe_context_set -> ContextSet.t -> [@@ocaml.deprecated "Use [Univ.extend_in_context_set]"] (** Create a fresh global in the global environment, without side effects. - BEWARE: this raises an ANOMALY on polymorphic constants/inductives: + BEWARE: this raises an error on polymorphic constants/inductives: the constraints should be properly added to an evd. See Evd.fresh_global, Evarutil.new_global, and pf_constr_of_global for - the proper way to get a fresh copy of a global reference. *) + the proper way to get a fresh copy of a polymorphic global reference. *) +val constr_of_monomorphic_global : GlobRef.t -> constr + val constr_of_global : GlobRef.t -> constr +[@@ocaml.deprecated "constr_of_global will crash on polymorphic constants,\ + use [constr_of_monomorphic_global] if the reference is guaranteed to\ + be monomorphic, [Evarutil.new_global] or [Tacmach.New.pf_constr_of_global] otherwise"] (** Returns the type of the global reference, by creating a fresh instance of polymorphic references and computing their instantiated universe context. (side-effect on the diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 98e1f6dd36..601099c6ff 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -26,7 +26,6 @@ open Notation_ops open Glob_term open Glob_ops open Pattern -open Nametab open Notation open Detyping open Decl_kinds @@ -213,7 +212,7 @@ let is_record indsp = with Not_found -> false let encode_record r = - let indsp = global_inductive r in + let indsp = Nametab.global_inductive r in if not (is_record indsp) then user_err ?loc:r.CAst.loc ~hdr:"encode_record" (str "This type is not a structure type."); @@ -279,7 +278,7 @@ let extern_evar n l = CEvar (n,l) may be inaccurate *) let default_extern_reference ?loc vars r = - shortest_qualid_of_global ?loc vars r + Nametab.shortest_qualid_of_global ?loc vars r let my_extern_reference = ref default_extern_reference @@ -481,7 +480,7 @@ and apply_notation_to_pattern ?loc gr ((subst,substlist),(nb_to_drop,more_args)) (make_pat_notation ?loc ntn (l,ll) l2') key) end | SynDefRule kn -> - let qid = shortest_qualid_of_syndef ?loc vars kn in + let qid = Nametab.shortest_qualid_of_syndef ?loc vars kn in let l1 = List.rev_map (fun (c,(subentry,(scopt,scl))) -> extern_cases_pattern_in_scope (subentry,(scopt,scl@scopes)) vars c) @@ -1136,7 +1135,7 @@ and extern_notation (custom,scopes as allscopes) vars t = function List.map (fun (c,(subentry,(scopt,scl))) -> extern true (subentry,(scopt,scl@snd scopes)) vars c, None) terms in - let a = CRef (shortest_qualid_of_syndef ?loc vars kn,None) in + let a = CRef (Nametab.shortest_qualid_of_syndef ?loc vars kn,None) in CAst.make ?loc @@ if List.is_empty l then a else CApp ((None, CAst.make a),l) in if List.is_empty args then e else diff --git a/interp/constrintern.ml b/interp/constrintern.ml index d7497d4e8e..6b22261a15 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -28,7 +28,6 @@ open Constrexpr open Constrexpr_ops open Notation_term open Notation_ops -open Nametab open Notation open Inductiveops open Decl_kinds @@ -633,7 +632,7 @@ let terms_of_binders bl = | PatVar (Name id) -> CRef (qualid_of_ident id, None) | PatVar (Anonymous) -> error_cannot_coerce_wildcard_term ?loc () | PatCstr (c,l,_) -> - let qid = qualid_of_path ?loc (path_of_global (ConstructRef c)) in + let qid = qualid_of_path ?loc (Nametab.path_of_global (ConstructRef c)) in let hole = CAst.make ?loc @@ CHole (None,IntroAnonymous,None) in let params = List.make (Inductiveops.inductive_nparams (fst c)) hole in CAppExpl ((None,qid,None),params @ List.map term_of_pat l)) pt in @@ -721,7 +720,7 @@ let instantiate_notation_constr loc intern intern_pat ntnvars subst infos c = try let gc = intern nenv c in Id.Map.add id (gc, Some c) map - with GlobalizationError _ -> map + with Nametab.GlobalizationError _ -> map in let mk_env' (c, (onlyident,(tmp_scope,subscopes))) = let nenv = {env with tmp_scope; scopes = subscopes @ env.scopes} in @@ -986,7 +985,7 @@ let intern_extended_global_of_qualid qid = let intern_reference qid = let r = try intern_extended_global_of_qualid qid - with Not_found -> error_global_not_found qid + with Not_found -> Nametab.error_global_not_found qid in Smartlocate.global_of_extended_global r @@ -1058,11 +1057,11 @@ let intern_applied_reference intern env namedctx (_, ntnvars as lvar) us args qi (* Extra allowance for non globalizing functions *) if !interning_grammar || env.unb then (gvar (loc,qualid_basename qid) us, [], [], []), args - else error_global_not_found qid + else Nametab.error_global_not_found qid else let r,projapp,args2 = try intern_qualid qid intern env ntnvars us args - with Not_found -> error_global_not_found qid + with Not_found -> Nametab.error_global_not_found qid in let x, imp, scopes, l = find_appl_head_data r in (x,imp,scopes,l), args2 @@ -1312,7 +1311,7 @@ let sort_fields ~complete loc fields completer = (* the reference constructor of the record *) let base_constructor = let global_record_id = ConstructRef record.Recordops.s_CONST in - try shortest_qualid_of_global ?loc Id.Set.empty global_record_id + try Nametab.shortest_qualid_of_global ?loc Id.Set.empty global_record_id with Not_found -> anomaly (str "Environment corruption for records.") in let () = check_duplicate loc fields in @@ -1493,7 +1492,7 @@ let drop_notations_pattern looked_for genv = in let rec drop_syndef top scopes qid pats = try - match locate_extended qid with + match Nametab.locate_extended qid with | SynDef sp -> let (vars,a) = Syntax_def.search_syntactic_definition sp in (match a with @@ -1550,7 +1549,7 @@ let drop_notations_pattern looked_for genv = | None -> raise (InternalizationError (loc,NotAConstructor head)) end | CPatCstr (qid, Some expl_pl, pl) -> - let g = try locate qid + let g = try Nametab.locate qid with Not_found -> raise (InternalizationError (loc,NotAConstructor qid)) in if expl_pl == [] then diff --git a/interp/declare.ml b/interp/declare.ml index 07a0066ea8..7a32018c0e 100644 --- a/interp/declare.ml +++ b/interp/declare.ml @@ -60,14 +60,7 @@ let open_constant i ((sp,kn), obj) = if obj.cst_locl then () else let con = Global.constant_of_delta_kn kn in - Nametab.push (Nametab.Exactly i) sp (ConstRef con); - match (Global.lookup_constant con).const_body with - | (Def _ | Undef _) -> () - | OpaqueDef lc -> - match Opaqueproof.get_constraints (Global.opaque_tables ()) lc with - | Some f when Future.is_val f -> - Global.push_context_set false (Future.force f) - | _ -> () + Nametab.push (Nametab.Exactly i) sp (ConstRef con) let exists_name id = variable_exists id || Global.exists_objlabel (Label.of_id id) diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index ab57176643..7a525f84a5 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -892,7 +892,9 @@ let bind_term_as_binding_env alp (terms,termlists,binders,binderlists as sigma) | GVar id' -> (if not (Id.equal id id') then (fst alp,(id,id')::snd alp) else alp), sigma - | _ -> anomaly (str "A term which can be a binder has to be a variable.") + | t -> + (* The term is a non-variable pattern *) + raise No_match with Not_found -> (* The matching against a term allowing to find the instance has not been found yet *) (* If it will be a different name, we shall unfortunately fail *) diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml index e3d490a1ad..b73d238c22 100644 --- a/interp/syntax_def.ml +++ b/interp/syntax_def.ml @@ -15,7 +15,6 @@ open Names open Libnames open Libobject open Lib -open Nametab open Notation_term (* Syntactic definitions. *) @@ -38,7 +37,7 @@ let load_syntax_constant i ((sp,kn),(_,pat,onlyparse)) = let is_alias_of_already_visible_name sp = function | _,NRef ref -> - let (dir,id) = repr_qualid (shortest_qualid_of_global Id.Set.empty ref) in + let (dir,id) = repr_qualid (Nametab.shortest_qualid_of_global Id.Set.empty ref) in DirPath.is_empty dir && Id.equal id (basename sp) | _ -> false @@ -83,11 +82,11 @@ let out_pat (ids,ac) = (List.map (fun (id,((_,sc),typ)) -> (id,sc)) ids,ac) let declare_syntactic_definition local id onlyparse pat = let _ = add_leaf id (in_syntax_constant (local,in_pat pat,onlyparse)) in () -let pr_syndef kn = pr_qualid (shortest_qualid_of_syndef Id.Set.empty kn) +let pr_syndef kn = pr_qualid (Nametab.shortest_qualid_of_syndef Id.Set.empty kn) let pr_compat_warning (kn, def, v) = let pp_def = match def with - | [], NRef r -> spc () ++ str "is" ++ spc () ++ pr_global_env Id.Set.empty r + | [], NRef r -> spc () ++ str "is" ++ spc () ++ Nametab.pr_global_env Id.Set.empty r | _ -> strbrk " is a compatibility notation" in pr_syndef kn ++ pp_def diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml index 819a66c190..c558689595 100644 --- a/kernel/cClosure.ml +++ b/kernel/cClosure.ml @@ -224,11 +224,6 @@ let unfold_red kn = * abstractions, storing a representation (of type 'a) of the body of * this constant or abstraction. * * i_tab is the cache table of the results - * * i_repr is the function to get the representation from the current - * state of the cache and the body of the constant. The result - * is stored in the table. - * * i_rels is the array of free rel variables together with their optional - * body * * ref_value_cache searchs in the tab, otherwise uses i_repr to * compute the result and store it in the table. If the constant can't @@ -256,74 +251,12 @@ end module KeyTable = Hashtbl.Make(IdKeyHash) -let eq_table_key = IdKeyHash.equal - -type 'a infos_tab = 'a KeyTable.t - -type 'a infos_cache = { - i_repr : 'a infos -> 'a infos_tab -> constr -> 'a; - i_env : env; - i_sigma : existential -> constr option; - i_rels : (Constr.rel_declaration * lazy_val) Range.t; - i_share : bool; -} - -and 'a infos = { - i_flags : reds; - i_cache : 'a infos_cache } - -let info_flags info = info.i_flags -let info_env info = info.i_cache.i_env - open Context.Named.Declaration let assoc_defined id env = match Environ.lookup_named id env with | LocalDef (_, c, _) -> c | _ -> raise Not_found -let ref_value_cache ({i_cache = cache;_} as infos) tab ref = - try - Some (KeyTable.find tab ref) - with Not_found -> - try - let body = - match ref with - | RelKey n -> - let open! Context.Rel.Declaration in - let i = n - 1 in - let (d, _) = - try Range.get cache.i_rels i - with Invalid_argument _ -> raise Not_found - in - begin match d with - | LocalAssum _ -> raise Not_found - | LocalDef (_, t, _) -> lift n t - end - | VarKey id -> assoc_defined id cache.i_env - | ConstKey cst -> constant_value_in cache.i_env cst - in - let v = cache.i_repr infos tab body in - KeyTable.add tab ref v; - Some v - with - | Not_found (* List.assoc *) - | NotEvaluableConst _ (* Const *) - -> None - -let evar_value cache ev = - cache.i_sigma ev - -let create ~repr ~share flgs env evars = - let cache = - { i_repr = repr; - i_env = env; - i_sigma = evars; - i_rels = env.env_rel_context.env_rel_map; - i_share = share; - } - in { i_flags = flgs; i_cache = cache } - - (**********************************************************************) (* Lazy reduction: the one used in kernel operations *) @@ -391,6 +324,23 @@ let update ~share v1 no t = v1) else {norm=no;term=t} +(** Reduction cache *) + +type infos_cache = { + i_env : env; + i_sigma : existential -> constr option; + i_share : bool; +} + +type clos_infos = { + i_flags : reds; + i_cache : infos_cache } + +type clos_tab = fconstr KeyTable.t + +let info_flags info = info.i_flags +let info_env info = info.i_cache.i_env + (**********************************************************************) (* The type of (machine) stacks (= lambda-bar-calculus' contexts) *) @@ -539,6 +489,8 @@ let mk_clos e t = | (CoFix _|Lambda _|Fix _|Prod _|Evar _|App _|Case _|Cast _|LetIn _|Proj _) -> {norm = Red; term = FCLOS(t,e)} +let inject c = mk_clos (subs_id 0) c + (** Hand-unrolling of the map function to bypass the call to the generic array allocation *) let mk_clos_vect env v = match v with @@ -550,6 +502,35 @@ let mk_clos_vect env v = match v with [|mk_clos env v0; mk_clos env v1; mk_clos env v2; mk_clos env v3|] | v -> Array.Fun1.map mk_clos env v +let ref_value_cache ({ i_cache = cache; _ }) tab ref = + try + Some (KeyTable.find tab ref) + with Not_found -> + try + let body = + match ref with + | RelKey n -> + let open! Context.Rel.Declaration in + let i = n - 1 in + let (d, _) = + try Range.get cache.i_env.env_rel_context.env_rel_map i + with Invalid_argument _ -> raise Not_found + in + begin match d with + | LocalAssum _ -> raise Not_found + | LocalDef (_, t, _) -> lift n t + end + | VarKey id -> assoc_defined id cache.i_env + | ConstKey cst -> constant_value_in cache.i_env cst + in + let v = inject body in + KeyTable.add tab ref v; + Some v + with + | Not_found (* List.assoc *) + | NotEvaluableConst _ (* Const *) + -> None + (* The inverse of mk_clos: move back to constr *) let rec to_constr lfts v = match v.term with @@ -944,7 +925,7 @@ let rec knr info tab m stk = | FLetIn (_,v,_,bd,e) when red_set info.i_flags fZETA -> knit info tab (subs_cons([|v|],e)) bd stk | FEvar(ev,env) -> - (match evar_value info.i_cache ev with + (match info.i_cache.i_sigma ev with Some c -> knit info tab env c stk | None -> (m,stk)) | FLOCKED | FRel _ | FAtom _ | FFlex _ | FInd _ | FApp _ | FProj _ @@ -1040,8 +1021,6 @@ let whd_val info tab v = let norm_val info tab v = with_stats (lazy (kl info tab v)) -let inject c = mk_clos (subs_id 0) c - let whd_stack infos tab m stk = match m.norm with | Whnf | Norm -> (** No need to perform [kni] nor to unlock updates because @@ -1052,19 +1031,19 @@ let whd_stack infos tab m stk = match m.norm with let () = if infos.i_cache.i_share then ignore (fapp_stack k) in (* to unlock Zupdates! *) k -(* cache of constants: the body is computed only when needed. *) -type clos_infos = fconstr infos - let create_clos_infos ?(evars=fun _ -> None) flgs env = let share = (Environ.typing_flags env).Declarations.share_reduction in - create ~share ~repr:(fun _ _ c -> inject c) flgs env evars + let cache = { + i_env = env; + i_sigma = evars; + i_share = share; + } in + { i_flags = flgs; i_cache = cache } let create_tab () = KeyTable.create 17 let oracle_of_infos infos = Environ.oracle infos.i_cache.i_env -let env_of_infos infos = infos.i_cache.i_env - let infos_with_reds infos reds = { infos with i_flags = reds } diff --git a/kernel/cClosure.mli b/kernel/cClosure.mli index 2a018d172a..1ee4bccc25 100644 --- a/kernel/cClosure.mli +++ b/kernel/cClosure.mli @@ -98,25 +98,7 @@ val unfold_red : evaluable_global_reference -> reds (***********************************************************************) type table_key = Constant.t Univ.puniverses tableKey -type 'a infos_cache -type 'a infos_tab -type 'a infos = { - i_flags : reds; - i_cache : 'a infos_cache } - -val ref_value_cache: 'a infos -> 'a infos_tab -> table_key -> 'a option -val create: - repr:('a infos -> 'a infos_tab -> constr -> 'a) -> - share:bool -> - reds -> - env -> - (existential -> constr option) -> - 'a infos -val create_tab : unit -> 'a infos_tab -val evar_value : 'a infos_cache -> existential -> constr option - -val info_env : 'a infos -> env -val info_flags: 'a infos -> reds +module KeyTable : Hashtbl.S with type key = table_key (*********************************************************************** s Lazy reduction. *) @@ -173,7 +155,6 @@ val stack_tail : int -> stack -> stack val stack_nth : stack -> int -> fconstr val zip_term : (fconstr -> constr) -> constr -> stack -> constr val eta_expand_stack : stack -> stack -val unfold_projection : 'a infos -> Projection.t -> stack_member option (** To lazy reduce a constr, create a [clos_infos] with [create_clos_infos], inject the term to reduce with [inject]; then use @@ -193,27 +174,32 @@ val destFLambda : (fconstr subs -> constr -> fconstr) -> fconstr -> Name.t * fconstr * fconstr (** Global and local constant cache *) -type clos_infos = fconstr infos +type clos_infos +type clos_tab val create_clos_infos : ?evars:(existential->constr option) -> reds -> env -> clos_infos val oracle_of_infos : clos_infos -> Conv_oracle.oracle -val env_of_infos : 'a infos -> env +val create_tab : unit -> clos_tab + +val info_env : clos_infos -> env +val info_flags: clos_infos -> reds +val unfold_projection : clos_infos -> Projection.t -> stack_member option val infos_with_reds : clos_infos -> reds -> clos_infos (** Reduction function *) (** [norm_val] is for strong normalization *) -val norm_val : clos_infos -> fconstr infos_tab -> fconstr -> constr +val norm_val : clos_infos -> clos_tab -> fconstr -> constr (** [whd_val] is for weak head normalization *) -val whd_val : clos_infos -> fconstr infos_tab -> fconstr -> constr +val whd_val : clos_infos -> clos_tab -> fconstr -> constr (** [whd_stack] performs weak head normalization in a given stack. It stops whenever a reduction is blocked. *) val whd_stack : - clos_infos -> fconstr infos_tab -> fconstr -> stack -> fconstr * stack + clos_infos -> clos_tab -> fconstr -> stack -> fconstr * stack (** [eta_expand_ind_stack env ind c s t] computes stacks correspoding to the conversion of the eta expansion of t, considered as an inhabitant @@ -230,9 +216,7 @@ val eta_expand_ind_stack : env -> inductive -> fconstr -> stack -> (** Conversion auxiliary functions to do step by step normalisation *) (** [unfold_reference] unfolds references in a [fconstr] *) -val unfold_reference : clos_infos -> fconstr infos_tab -> table_key -> fconstr option - -val eq_table_key : table_key -> table_key -> bool +val unfold_reference : clos_infos -> clos_tab -> table_key -> fconstr option (*********************************************************************** i This is for lazy debug *) @@ -243,9 +227,9 @@ val lift_fconstr_vect : int -> fconstr array -> fconstr array val mk_clos : fconstr subs -> constr -> fconstr val mk_clos_vect : fconstr subs -> constr array -> fconstr array -val kni: clos_infos -> fconstr infos_tab -> fconstr -> stack -> fconstr * stack -val knr: clos_infos -> fconstr infos_tab -> fconstr -> stack -> fconstr * stack -val kl : clos_infos -> fconstr infos_tab -> fconstr -> constr +val kni: clos_infos -> clos_tab -> fconstr -> stack -> fconstr * stack +val knr: clos_infos -> clos_tab -> fconstr -> stack -> fconstr * stack +val kl : clos_infos -> clos_tab -> fconstr -> constr val to_constr : lift -> fconstr -> constr diff --git a/kernel/constr.ml b/kernel/constr.ml index b490aa5092..d7f35da10d 100644 --- a/kernel/constr.ml +++ b/kernel/constr.ml @@ -452,6 +452,27 @@ let fold f acc c = match kind c with | CoFix (_,(_lna,tl,bl)) -> Array.fold_left2 (fun acc t b -> f (f acc t) b) acc tl bl +let fold_with_full_binders g f n acc c = + let open Context.Rel.Declaration in + match kind c with + | Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _ | Construct _ -> acc + | Cast (c,_, t) -> f n (f n acc c) t + | Prod (na,t,c) -> f (g (LocalAssum (na,t)) n) (f n acc t) c + | Lambda (na,t,c) -> f (g (LocalAssum (na,t)) n) (f n acc t) c + | LetIn (na,b,t,c) -> f (g (LocalDef (na,b,t)) n) (f n (f n acc b) t) c + | App (c,l) -> Array.fold_left (f n) (f n acc c) l + | Proj (_,c) -> f n acc c + | Evar (_,l) -> Array.fold_left (f n) acc l + | Case (_,p,c,bl) -> Array.fold_left (f n) (f n (f n acc p) c) bl + | Fix (_,(lna,tl,bl)) -> + let n' = CArray.fold_left2 (fun c n t -> g (LocalAssum (n,t)) c) n lna tl in + let fd = Array.map2 (fun t b -> (t,b)) tl bl in + Array.fold_left (fun acc (t,b) -> f n' (f n acc t) b) acc fd + | CoFix (_,(lna,tl,bl)) -> + let n' = CArray.fold_left2 (fun c n t -> g (LocalAssum (n,t)) c) n lna tl in + let fd = Array.map2 (fun t b -> (t,b)) tl bl in + Array.fold_left (fun acc (t,b) -> f n' (f n acc t) b) acc fd + (* [iter f c] iters [f] on the immediate subterms of [c]; it is not recursive and the order with which subterms are processed is not specified *) diff --git a/kernel/constr.mli b/kernel/constr.mli index c012f04260..8753c20eac 100644 --- a/kernel/constr.mli +++ b/kernel/constr.mli @@ -470,6 +470,10 @@ val map_return_predicate_with_full_binders : ((constr, constr) Context.Rel.Decla val fold : ('a -> constr -> 'a) -> 'a -> constr -> 'a +val fold_with_full_binders : + (rel_declaration -> 'a -> 'a) -> ('a -> 'b -> constr -> 'b) -> + 'a -> 'b -> constr -> 'b + (** [map f c] maps [f] on the immediate subterms of [c]; it is not recursive and the order with which subterms are processed is not specified *) diff --git a/kernel/conv_oracle.ml b/kernel/conv_oracle.ml index c74f2ab318..ac78064235 100644 --- a/kernel/conv_oracle.ml +++ b/kernel/conv_oracle.ml @@ -83,18 +83,27 @@ let fold_strategy f { var_opacity; cst_opacity; _ } accu = let get_transp_state { var_trstate; cst_trstate; _ } = (var_trstate, cst_trstate) +let dep_order l2r k1 k2 = match k1, k2 with +| RelKey _, RelKey _ -> l2r +| RelKey _, (VarKey _ | ConstKey _) -> true +| VarKey _, RelKey _ -> false +| VarKey _, VarKey _ -> l2r +| VarKey _, ConstKey _ -> true +| ConstKey _, (RelKey _ | VarKey _) -> false +| ConstKey _, ConstKey _ -> l2r + (* Unfold the first constant only if it is "more transparent" than the second one. In case of tie, use the recommended default. *) let oracle_order f o l2r k1 k2 = match get_strategy o f k1, get_strategy o f k2 with - | Expand, Expand -> l2r + | Expand, Expand -> dep_order l2r k1 k2 | Expand, (Opaque | Level _) -> true | (Opaque | Level _), Expand -> false - | Opaque, Opaque -> l2r + | Opaque, Opaque -> dep_order l2r k1 k2 | Level _, Opaque -> true | Opaque, Level _ -> false | Level n1, Level n2 -> - if Int.equal n1 n2 then l2r + if Int.equal n1 n2 then dep_order l2r k1 k2 else n1 < n2 let get_strategy o = get_strategy o (fun x -> x) diff --git a/kernel/reduction.ml b/kernel/reduction.ml index 00576476ab..18697d07e5 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -316,8 +316,8 @@ let compare_stacks f fmind lft1 stk1 lft2 stk2 cuniv = type conv_tab = { cnv_inf : clos_infos; - lft_tab : fconstr infos_tab; - rgt_tab : fconstr infos_tab; + lft_tab : clos_tab; + rgt_tab : clos_tab; } (** Invariant: for any tl ∈ lft_tab and tr ∈ rgt_tab, there is no mutable memory location contained both in tl and in tr. *) @@ -346,7 +346,7 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = | (Sort s1, Sort s2) -> if not (is_empty_stack v1 && is_empty_stack v2) then anomaly (Pp.str "conversion was given ill-typed terms (Sort)."); - sort_cmp_universes (env_of_infos infos.cnv_inf) cv_pb s1 s2 cuniv + sort_cmp_universes (info_env infos.cnv_inf) cv_pb s1 s2 cuniv | (Meta n, Meta m) -> if Int.equal n m then convert_stacks l2r infos lft1 lft2 v1 v2 cuniv diff --git a/library/coqlib.ml b/library/coqlib.ml index 677515981a..a044a9a395 100644 --- a/library/coqlib.ml +++ b/library/coqlib.ml @@ -14,7 +14,6 @@ open Pp open Names open Libnames open Globnames -open Nametab let make_dir l = DirPath.make (List.rev_map Id.of_string l) @@ -79,7 +78,7 @@ let register_ref s c = (* Generic functions to find Coq objects *) let has_suffix_in_dirs dirs ref = - let dir = dirpath (path_of_global ref) in + let dir = dirpath (Nametab.path_of_global ref) in List.exists (fun d -> is_dirpath_prefix_of d dir) dirs let gen_reference_in_modules locstr dirs s = diff --git a/man/coq-interface.1 b/man/coq-interface.1 deleted file mode 100644 index ee013d952e..0000000000 --- a/man/coq-interface.1 +++ /dev/null @@ -1,37 +0,0 @@ -.TH COQ 1 "April 25, 2001" - -.SH NAME -coq\-interface \- Customized Coq toplevel to make user interfaces - - -.SH SYNOPSIS -.B coq-interface -[ -.B options -] - -.SH DESCRIPTION - -.B coq-interface -is a Coq customized toplevel system for Coq containing some modules -useful for the graphical interface. This program is not for the casual -user. - -.SH OPTIONS - -.TP -.B \-h -Help. Will give you the complete list of options accepted by -coq-interface (the same as coqtop). - -.SH SEE ALSO - -.BR coqc (1), -.BR coqdep (1), -.BR coqtop (1), -.BR coq\-parser (1). -.br -.I -The Coq Reference Manual. -.I -The Coq web site: http://coq.inria.fr diff --git a/man/coq-parser.1 b/man/coq-parser.1 deleted file mode 100644 index 23dc820193..0000000000 --- a/man/coq-parser.1 +++ /dev/null @@ -1,30 +0,0 @@ -.TH COQ 1 "April 25, 2001" - -.SH NAME -coq\-parser \- Coq parser - - -.SH SYNOPSIS -.B coq\-parser -[ -.B options -] - -.SH DESCRIPTION - -.B parser -is a program reading Coq proof developments and outputing them in the -structured format given in the INRIA technical report RT154. This -program is not for the casual user. - -.SH SEE ALSO - -.BR coq\-interface (1), -.BR coqc (1), -.BR coqtop (1), -.BR coqdep (1). -.br -.I -The Coq Reference Manual. -.I -The Coq web site: http://coq.inria.fr diff --git a/man/dune b/man/dune new file mode 100644 index 0000000000..359e780545 --- /dev/null +++ b/man/dune @@ -0,0 +1,10 @@ +(install + (section man) + (package coq) + (files coqc.1 coqtop.1 coqtop.byte.1 coqtop.opt.1 coqchk.1 coqdep.1 coqdoc.1 coq_makefile.1 coq-tex.1 coqwc.1)) + +(install + (section man) + (package coqide) + (files coqide.1)) + diff --git a/parsing/dune b/parsing/dune index b70612a52b..f931321358 100644 --- a/parsing/dune +++ b/parsing/dune @@ -5,11 +5,6 @@ (libraries proofs)) (rule - (targets cLexer.ml) - (deps (:ml4-file cLexer.ml4)) - (action (run camlp5o -loc loc -impl %{ml4-file} -o %{targets}))) - -(rule (targets g_prim.ml) (deps (:mlg-file g_prim.mlg)) (action (run coqpp %{mlg-file}))) diff --git a/plugins/btauto/refl_btauto.ml b/plugins/btauto/refl_btauto.ml index b9ad1ff6d8..07f50f6cd5 100644 --- a/plugins/btauto/refl_btauto.ml +++ b/plugins/btauto/refl_btauto.ml @@ -10,7 +10,7 @@ open Constr -let bt_lib_constr n = lazy (UnivGen.constr_of_global @@ Coqlib.lib_ref n) +let bt_lib_constr n = lazy (UnivGen.constr_of_monomorphic_global @@ Coqlib.lib_ref n) let decomp_term sigma (c : Constr.t) = Constr.kind (EConstr.Unsafe.to_constr (Termops.strip_outer_cast sigma (EConstr.of_constr c))) diff --git a/plugins/firstorder/rules.ml b/plugins/firstorder/rules.ml index 8fa676de44..b0c4785d7a 100644 --- a/plugins/firstorder/rules.ml +++ b/plugins/firstorder/rules.ml @@ -233,12 +233,11 @@ let ll_forall_tac prod backtrack id continue seq= (* special for compatibility with old Intuition *) -let constant str = UnivGen.constr_of_global - @@ Coqlib.lib_ref str +let constant str = Coqlib.lib_ref str let defined_connectives = lazy - [AllOccurrences, EvalConstRef (fst (Constr.destConst (constant "core.not.type"))); - AllOccurrences, EvalConstRef (fst (Constr.destConst (constant "core.iff.type")))] + [AllOccurrences, EvalConstRef (destConstRef (constant "core.not.type")); + AllOccurrences, EvalConstRef (destConstRef (constant "core.iff.type"))] let normalize_evaluables= Proofview.Goal.enter begin fun gl -> diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index 98d68d3db7..ad1114b733 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -414,9 +414,9 @@ let rewrite_until_var arg_num eq_ids : tactic = let rec_pte_id = Id.of_string "Hrec" let clean_hyp_with_heq ptes_infos eq_hyps hyp_id env sigma = - let coq_False = EConstr.of_constr (UnivGen.constr_of_global @@ Coqlib.lib_ref "core.False.type") in - let coq_True = EConstr.of_constr (UnivGen.constr_of_global @@ Coqlib.lib_ref "core.True.type") in - let coq_I = EConstr.of_constr (UnivGen.constr_of_global @@ Coqlib.lib_ref "core.True.I") in + let coq_False = EConstr.of_constr (UnivGen.constr_of_monomorphic_global @@ Coqlib.lib_ref "core.False.type") in + let coq_True = EConstr.of_constr (UnivGen.constr_of_monomorphic_global @@ Coqlib.lib_ref "core.True.type") in + let coq_I = EConstr.of_constr (UnivGen.constr_of_monomorphic_global @@ Coqlib.lib_ref "core.True.I") in let rec scan_type context type_of_hyp : tactic = if isLetIn sigma type_of_hyp then let real_type_of_hyp = it_mkProd_or_LetIn type_of_hyp context in @@ -1605,7 +1605,7 @@ let prove_principle_for_gen match !tcc_lemma_ref with | Undefined -> user_err Pp.(str "No tcc proof !!") | Value lemma -> EConstr.of_constr lemma - | Not_needed -> EConstr.of_constr (UnivGen.constr_of_global @@ Coqlib.lib_ref "core.True.I") + | Not_needed -> EConstr.of_constr (UnivGen.constr_of_monomorphic_global @@ Coqlib.lib_ref "core.True.I") in (* let rec list_diff del_list check_list = *) (* match del_list with *) diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index 03a64988e4..a385a61ae0 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -116,7 +116,7 @@ let def_of_const t = [@@@ocaml.warning "-3"] let coq_constant s = - UnivGen.constr_of_global @@ + UnivGen.constr_of_monomorphic_global @@ Coqlib.gen_reference_in_modules "RecursiveDefinition" Coqlib.init_modules s;; @@ -441,7 +441,7 @@ let jmeq () = try Coqlib.check_required_library Coqlib.jmeq_module_name; EConstr.of_constr @@ - UnivGen.constr_of_global @@ + UnivGen.constr_of_monomorphic_global @@ Coqlib.lib_ref "core.JMeq.type" with e when CErrors.noncritical e -> raise (ToShow e) @@ -449,7 +449,7 @@ let jmeq_refl () = try Coqlib.check_required_library Coqlib.jmeq_module_name; EConstr.of_constr @@ - UnivGen.constr_of_global @@ + UnivGen.constr_of_monomorphic_global @@ Coqlib.lib_ref "core.JMeq.refl" with e when CErrors.noncritical e -> raise (ToShow e) @@ -463,7 +463,7 @@ let acc_rel = function () -> EConstr.of_constr (coq_constant "Acc") let acc_inv_id = function () -> EConstr.of_constr (coq_constant "Acc_inv") [@@@ocaml.warning "-3"] -let well_founded_ltof () = EConstr.of_constr @@ UnivGen.constr_of_global @@ +let well_founded_ltof () = EConstr.of_constr @@ UnivGen.constr_of_monomorphic_global @@ Coqlib.find_reference "IndFun" ["Coq"; "Arith";"Wf_nat"] "well_founded_ltof" [@@@ocaml.warning "+3"] diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index b8973a18dc..b0842c3721 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -81,7 +81,7 @@ let thin ids gl = Proofview.V82.of_tactic (Tactics.clear ids) gl let make_eq () = try - EConstr.of_constr (UnivGen.constr_of_global (Coqlib.lib_ref "core.eq.type")) + EConstr.of_constr (UnivGen.constr_of_monomorphic_global (Coqlib.lib_ref "core.eq.type")) with _ -> assert false (* [generate_type g_to_f f graph i] build the completeness (resp. correctness) lemma type if [g_to_f = true] @@ -511,7 +511,7 @@ and intros_with_rewrite_aux : Tacmach.tactic = intros_with_rewrite ] g end - | Ind _ when EConstr.eq_constr sigma t (EConstr.of_constr (UnivGen.constr_of_global @@ Coqlib.lib_ref "core.False.type")) -> + | Ind _ when EConstr.eq_constr sigma t (EConstr.of_constr (UnivGen.constr_of_monomorphic_global @@ Coqlib.lib_ref "core.False.type")) -> Proofview.V82.of_tactic tauto g | Case(_,_,v,_) -> tclTHENLIST[ diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index ca3160f4c4..f9df3aed45 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -51,7 +51,7 @@ open Context.Rel.Declaration (* Ugly things which should not be here *) [@@@ocaml.warning "-3"] -let coq_constant m s = EConstr.of_constr @@ constr_of_global @@ +let coq_constant m s = EConstr.of_constr @@ UnivGen.constr_of_monomorphic_global @@ Coqlib.find_reference "RecursiveDefinition" m s let arith_Nat = ["Coq"; "Arith";"PeanoNat";"Nat"] @@ -63,7 +63,7 @@ let pr_leconstr_rd = let coq_init_constant s = EConstr.of_constr ( - constr_of_global @@ + UnivGen.constr_of_monomorphic_global @@ Coqlib.gen_reference_in_modules "RecursiveDefinition" Coqlib.init_modules s) [@@@ocaml.warning "+3"] @@ -97,7 +97,7 @@ let type_of_const sigma t = Typeops.type_of_constant_in (Global.env()) (sp, u) |_ -> assert false -let constant sl s = constr_of_global (find_reference sl s) +let constant sl s = UnivGen.constr_of_monomorphic_global (find_reference sl s) let const_of_ref = function ConstRef kn -> kn @@ -1241,7 +1241,7 @@ let get_current_subgoals_types () = exception EmptySubgoals let build_and_l sigma l = - let and_constr = UnivGen.constr_of_global @@ Coqlib.lib_ref "core.and.type" in + let and_constr = UnivGen.constr_of_monomorphic_global @@ Coqlib.lib_ref "core.and.type" in let conj_constr = Coqlib.build_coq_conj () in let mk_and p1 p2 = mkApp(EConstr.of_constr and_constr,[|p1;p2|]) in diff --git a/plugins/ltac/tacenv.ml b/plugins/ltac/tacenv.ml index 1f2c722b34..a88285c9ee 100644 --- a/plugins/ltac/tacenv.ml +++ b/plugins/ltac/tacenv.ml @@ -115,7 +115,6 @@ let interp_ml_tactic { mltac_name = s; mltac_index = i } = (* Summary and Object declaration *) -open Nametab open Libobject type ltac_entry = { @@ -153,19 +152,19 @@ let tac_deprecation kn = let load_md i ((sp, kn), (local, id, b, t, deprecation)) = match id with | None -> - let () = if not local then push_tactic (Until i) sp kn in + let () = if not local then push_tactic (Nametab.Until i) sp kn in add ~deprecation kn b t | Some kn0 -> replace kn0 kn t let open_md i ((sp, kn), (local, id, b, t, deprecation)) = match id with | None -> - let () = if not local then push_tactic (Exactly i) sp kn in + let () = if not local then push_tactic (Nametab.Exactly i) sp kn in add ~deprecation kn b t | Some kn0 -> replace kn0 kn t let cache_md ((sp, kn), (local, id ,b, t, deprecation)) = match id with | None -> - let () = push_tactic (Until 1) sp kn in + let () = push_tactic (Nametab.Until 1) sp kn in add ~deprecation kn b t | Some kn0 -> replace kn0 kn t diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml index 5501cf92a5..55412c74bb 100644 --- a/plugins/ltac/tacintern.ml +++ b/plugins/ltac/tacintern.ml @@ -19,7 +19,6 @@ open Util open Names open Libnames open Globnames -open Nametab open Smartlocate open Constrexpr open Termops @@ -98,7 +97,7 @@ let intern_global_reference ist qid = ArgVar (make ?loc:qid.CAst.loc @@ qualid_basename qid) else try ArgArg (qid.CAst.loc,locate_global_with_alias qid) - with Not_found -> error_global_not_found qid + with Not_found -> Nametab.error_global_not_found qid let intern_ltac_variable ist qid = if qualid_is_ident qid && find_var (qualid_basename qid) ist then @@ -150,7 +149,7 @@ let intern_isolated_tactic_reference strict ist qid = try ConstrMayEval (ConstrTerm (intern_constr_reference strict ist qid)) with Not_found -> (* Reference not found *) - error_global_not_found qid + Nametab.error_global_not_found qid (* Internalize an applied tactic reference *) @@ -169,7 +168,7 @@ let intern_applied_tactic_reference ist qid = try intern_applied_global_tactic_reference qid with Not_found -> (* Reference not found *) - error_global_not_found qid + Nametab.error_global_not_found qid (* Intern a reference parsed in a non-tactic entry *) @@ -190,7 +189,7 @@ let intern_non_tactic_reference strict ist qid = TacGeneric ipat else (* Reference not found *) - error_global_not_found qid + Nametab.error_global_not_found qid let intern_message_token ist = function | (MsgString _ | MsgInt _ as x) -> x @@ -302,7 +301,7 @@ let intern_evaluable_global_reference ist qid = try evaluable_of_global_reference ist.genv (locate_global_with_alias ~head:true qid) with Not_found -> if qualid_is_ident qid && not !strict_check then EvalVarRef (qualid_basename qid) - else error_global_not_found qid + else Nametab.error_global_not_found qid let intern_evaluable_reference_or_by_notation ist = function | {v=AN r} -> intern_evaluable_global_reference ist r @@ -377,7 +376,7 @@ let intern_typed_pattern_or_ref_with_occurrences ist (l,p) = subterm matched when a pattern *) let r = match r with | {v=AN r} -> r - | {loc} -> (qualid_of_path ?loc (path_of_global (smart_global r))) in + | {loc} -> (qualid_of_path ?loc (Nametab.path_of_global (smart_global r))) in let sign = { Constrintern.ltac_vars = ist.ltacvars; ltac_bound = Id.Set.empty; diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index f90e889678..b60b77595b 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -23,7 +23,6 @@ open Names open Nameops open Libnames open Globnames -open Nametab open Refiner open Tacmach.New open Tactic_debug @@ -358,7 +357,7 @@ let interp_reference ist env sigma = function with Not_found -> try VarRef (get_id (Environ.lookup_named id env)) - with Not_found -> error_global_not_found (qualid_of_ident ?loc id) + with Not_found -> Nametab.error_global_not_found (qualid_of_ident ?loc id) let try_interp_evaluable env (loc, id) = let v = Environ.lookup_named id env in @@ -374,14 +373,14 @@ let interp_evaluable ist env sigma = function with Not_found -> match r with | EvalConstRef _ -> r - | _ -> error_global_not_found (qualid_of_ident ?loc id) + | _ -> Nametab.error_global_not_found (qualid_of_ident ?loc id) end | ArgArg (r,None) -> r | ArgVar {loc;v=id} -> try try_interp_ltac_var (coerce_to_evaluable_ref env sigma) ist (Some (env,sigma)) (make ?loc id) with Not_found -> try try_interp_evaluable env (loc, id) - with Not_found -> error_global_not_found (qualid_of_ident ?loc id) + with Not_found -> Nametab.error_global_not_found (qualid_of_ident ?loc id) (* Interprets an hypothesis name *) let interp_occurrences ist occs = @@ -640,7 +639,7 @@ let interp_closed_typed_pattern_with_occurrences ist env sigma (occs, a) = Inr (pattern_of_constr env sigma (EConstr.to_constr sigma c)) in (try try_interp_ltac_var coerce_eval_ref_or_constr ist (Some (env,sigma)) (make ?loc id) with Not_found -> - error_global_not_found (qualid_of_ident ?loc id)) + Nametab.error_global_not_found (qualid_of_ident ?loc id)) | Inl (ArgArg _ as b) -> Inl (interp_evaluable ist env sigma b) | Inr c -> Inr (interp_typed_pattern ist env sigma c) in interp_occurrences ist occs, p diff --git a/plugins/nsatz/nsatz.ml b/plugins/nsatz/nsatz.ml index 11d0a4a44d..ef60a23e80 100644 --- a/plugins/nsatz/nsatz.ml +++ b/plugins/nsatz/nsatz.ml @@ -135,7 +135,7 @@ let mul = function | (Const n,q) when eq_num n num_1 -> q | (p,q) -> Mul(p,q) -let gen_constant n = lazy (UnivGen.constr_of_global (Coqlib.lib_ref n)) +let gen_constant n = lazy (UnivGen.constr_of_monomorphic_global (Coqlib.lib_ref n)) let tpexpr = gen_constant "plugins.setoid_ring.pexpr" let ttconst = gen_constant "plugins.setoid_ring.const" @@ -540,7 +540,7 @@ let nsatz lpol = let return_term t = let a = - mkApp (UnivGen.constr_of_global @@ Coqlib.lib_ref "core.eq.refl",[|tllp ();t|]) in + mkApp (UnivGen.constr_of_monomorphic_global @@ Coqlib.lib_ref "core.eq.refl",[|tllp ();t|]) in let a = EConstr.of_constr a in generalize [a] diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml index 09bd4cd352..d8adb17710 100644 --- a/plugins/omega/coq_omega.ml +++ b/plugins/omega/coq_omega.ml @@ -186,7 +186,8 @@ let reset_all () = To use the constant Zplus, one must type "Lazy.force coq_Zplus" This is the right way to access to Coq constants in tactics ML code *) -let gen_constant k = lazy (k |> Coqlib.lib_ref |> UnivGen.constr_of_global |> EConstr.of_constr) +let gen_constant k = lazy (k |> Coqlib.lib_ref |> UnivGen.constr_of_monomorphic_global + |> EConstr.of_constr) (* Zarith *) diff --git a/plugins/rtauto/refl_tauto.ml b/plugins/rtauto/refl_tauto.ml index 79418da27c..840a05e02b 100644 --- a/plugins/rtauto/refl_tauto.ml +++ b/plugins/rtauto/refl_tauto.ml @@ -26,11 +26,11 @@ let step_count = ref 0 let node_count = ref 0 -let li_False = lazy (destInd (UnivGen.constr_of_global @@ Coqlib.lib_ref "core.False.type")) -let li_and = lazy (destInd (UnivGen.constr_of_global @@ Coqlib.lib_ref "core.and.type")) -let li_or = lazy (destInd (UnivGen.constr_of_global @@ Coqlib.lib_ref "core.or.type")) +let li_False = lazy (destInd (UnivGen.constr_of_monomorphic_global @@ Coqlib.lib_ref "core.False.type")) +let li_and = lazy (destInd (UnivGen.constr_of_monomorphic_global @@ Coqlib.lib_ref "core.and.type")) +let li_or = lazy (destInd (UnivGen.constr_of_monomorphic_global @@ Coqlib.lib_ref "core.or.type")) -let gen_constant n = lazy (UnivGen.constr_of_global (Coqlib.lib_ref n)) +let gen_constant n = lazy (UnivGen.constr_of_monomorphic_global (Coqlib.lib_ref n)) let l_xI = gen_constant "num.pos.xI" let l_xO = gen_constant "num.pos.xO" diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml index 9585826109..8dbef47fe1 100644 --- a/plugins/setoid_ring/newring.ml +++ b/plugins/setoid_ring/newring.ml @@ -206,7 +206,7 @@ let exec_tactic env evd n f args = let nf c = constr_of evd c in Array.map nf !tactic_res, Evd.universe_context_set evd -let gen_constant n = lazy (EConstr.of_constr (UnivGen.constr_of_global (Coqlib.lib_ref n))) +let gen_constant n = lazy (EConstr.of_constr (UnivGen.constr_of_monomorphic_global (Coqlib.lib_ref n))) let gen_reference n = lazy (Coqlib.lib_ref n) let coq_mk_Setoid = gen_constant "plugins.setoid_ring.Build_Setoid_Theory" @@ -251,7 +251,7 @@ let plugin_modules = ] let my_constant c = - lazy (EConstr.of_constr (UnivGen.constr_of_global @@ Coqlib.gen_reference_in_modules "Ring" plugin_modules c)) + lazy (EConstr.of_constr (UnivGen.constr_of_monomorphic_global @@ Coqlib.gen_reference_in_modules "Ring" plugin_modules c)) [@@ocaml.warning "-3"] let my_reference c = lazy (Coqlib.gen_reference_in_modules "Ring" plugin_modules c) @@ -901,7 +901,7 @@ let ftheory_to_obj : field_info -> obj = let field_equality evd r inv req = match EConstr.kind !evd req with | App (f, [| _ |]) when eq_constr_nounivs !evd f (Lazy.force coq_eq) -> - let c = UnivGen.constr_of_global Coqlib.(lib_ref "core.eq.congr") in + let c = UnivGen.constr_of_monomorphic_global Coqlib.(lib_ref "core.eq.congr") in let c = EConstr.of_constr c in mkApp(c,[|r;r;inv|]) | _ -> diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml index 1492cfb4e4..6746eff223 100644 --- a/plugins/ssr/ssrcommon.ml +++ b/plugins/ssr/ssrcommon.ml @@ -1220,7 +1220,7 @@ let genclrtac cl cs clr = (fun type_err gl -> tclTHEN (tclTHEN (Proofview.V82.of_tactic (Tactics.elim_type (EConstr.of_constr - (UnivGen.constr_of_global @@ Coqlib.(lib_ref "core.False.type"))))) (old_cleartac clr)) + (UnivGen.constr_of_monomorphic_global @@ Coqlib.(lib_ref "core.False.type"))))) (old_cleartac clr)) (fun gl -> raise type_err) gl)) (old_cleartac clr) diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml index 265909980b..5061aeff88 100644 --- a/pretyping/cbv.ml +++ b/pretyping/cbv.ml @@ -134,7 +134,12 @@ let mkSTACK = function | STACK(0,v0,stk0), stk -> STACK(0,v0,stack_concat stk0 stk) | v,stk -> STACK(0,v,stk) -type cbv_infos = { tab : cbv_value infos_tab; infos : cbv_value infos; sigma : Evd.evar_map } +type cbv_infos = { + env : Environ.env; + tab : cbv_value KeyTable.t; + reds : RedFlags.reds; + sigma : Evd.evar_map +} (* Change: zeta reduction cannot be avoided in CBV *) @@ -260,8 +265,8 @@ let rec norm_head info env t stack = | Proj (p, c) -> let p' = - if red_set (info_flags info.infos) (fCONST (Projection.constant p)) - && red_set (info_flags info.infos) fBETA + if red_set info.reds (fCONST (Projection.constant p)) + && red_set info.reds fBETA then Projection.unfold p else p in @@ -280,16 +285,16 @@ let rec norm_head info env t stack = | Var id -> norm_head_ref 0 info env stack (VarKey id) | Const sp -> - Reductionops.reduction_effect_hook (env_of_infos info.infos) info.sigma + Reductionops.reduction_effect_hook info.env info.sigma (fst sp) (lazy (reify_stack t stack)); norm_head_ref 0 info env stack (ConstKey sp) | LetIn (_, b, _, c) -> (* zeta means letin are contracted; delta without zeta means we *) (* allow bindings but leave let's in place *) - if red_set (info_flags info.infos) fZETA then + if red_set info.reds fZETA then (* New rule: for Cbv, Delta does not apply to locally bound variables - or red_set (info_flags info.infos) fDELTA + or red_set info.reds fDELTA *) let env' = subs_cons ([|cbv_stack_term info TOP env b|],env) in norm_head info env' c stack @@ -297,7 +302,7 @@ let rec norm_head info env t stack = (CBN(t,env), stack) (* Should we consider a commutative cut ? *) | Evar ev -> - (match evar_value info.infos.i_cache ev with + (match Reductionops.safe_evar_value info.sigma ev with Some c -> norm_head info env c stack | None -> let e, xs = ev in @@ -317,8 +322,8 @@ let rec norm_head info env t stack = | Prod _ -> (CBN(t,env), stack) and norm_head_ref k info env stack normt = - if red_set_ref (info_flags info.infos) normt then - match ref_value_cache info.infos info.tab normt with + if red_set_ref info.reds normt then + match cbv_value_cache info normt with | Some body -> if !debug_cbv then Feedback.msg_debug Pp.(str "Unfolding " ++ debug_pr_key normt); strip_appl (shift_value k body) stack @@ -343,7 +348,7 @@ and cbv_stack_term info stack env t = and cbv_stack_value info env = function (* a lambda meets an application -> BETA *) | (LAM (nlams,ctxt,b,env), APP (args, stk)) - when red_set (info_flags info.infos) fBETA -> + when red_set info.reds fBETA -> let nargs = Array.length args in if nargs == nlams then cbv_stack_term info stk (subs_cons(args,env)) b @@ -357,31 +362,31 @@ and cbv_stack_value info env = function (* a Fix applied enough -> IOTA *) | (FIXP(fix,env,[||]), stk) - when fixp_reducible (info_flags info.infos) fix stk -> + when fixp_reducible info.reds fix stk -> let (envf,redfix) = contract_fixp env fix in cbv_stack_term info stk envf redfix (* constructor guard satisfied or Cofix in a Case -> IOTA *) | (COFIXP(cofix,env,[||]), stk) - when cofixp_reducible (info_flags info.infos) cofix stk-> + when cofixp_reducible info.reds cofix stk-> let (envf,redfix) = contract_cofixp env cofix in cbv_stack_term info stk envf redfix (* constructor in a Case -> IOTA *) | (CONSTR(((sp,n),u),[||]), APP(args,CASE(_,br,ci,env,stk))) - when red_set (info_flags info.infos) fMATCH -> + when red_set info.reds fMATCH -> let cargs = Array.sub args ci.ci_npar (Array.length args - ci.ci_npar) in cbv_stack_term info (stack_app cargs stk) env br.(n-1) (* constructor of arity 0 in a Case -> IOTA *) | (CONSTR(((_,n),u),[||]), CASE(_,br,_,env,stk)) - when red_set (info_flags info.infos) fMATCH -> + when red_set info.reds fMATCH -> cbv_stack_term info stk env br.(n-1) (* constructor in a Projection -> IOTA *) | (CONSTR(((sp,n),u),[||]), APP(args,PROJ(p,stk))) - when red_set (info_flags info.infos) fMATCH && Projection.unfolded p -> + when red_set info.reds fMATCH && Projection.unfolded p -> let arg = args.(Projection.npars p + Projection.arg p) in cbv_stack_value info env (strip_appl arg stk) @@ -393,6 +398,29 @@ and cbv_stack_value info env = function (* definitely a value *) | (head,stk) -> mkSTACK(head, stk) +and cbv_value_cache info ref = match KeyTable.find info.tab ref with +| v -> Some v +| exception Not_found -> + try + let body = match ref with + | RelKey n -> + let open Context.Rel.Declaration in + begin match Environ.lookup_rel n info.env with + | LocalDef (_, c, _) -> lift n c + | LocalAssum _ -> raise Not_found + end + | VarKey id -> + let open Context.Named.Declaration in + begin match Environ.lookup_named id info.env with + | LocalDef (_, c, _) -> c + | LocalAssum _ -> raise Not_found + end + | ConstKey cst -> Environ.constant_value_in info.env cst + in + let v = cbv_stack_term info TOP (subs_id 0) body in + let () = KeyTable.add info.tab ref v in + Some v + with Not_found | Environ.NotEvaluableConst _ -> None (* When we are sure t will never produce a redex with its stack, we * normalize (even under binders) the applied terms and we build the @@ -453,11 +481,5 @@ let cbv_norm infos constr = EConstr.of_constr (with_stats (lazy (cbv_norm_term infos (subs_id 0) constr))) (* constant bodies are normalized at the first expansion *) -let create_cbv_infos flgs env sigma = - let infos = create - ~share:true (** Not used by cbv *) - ~repr:(fun old_info tab c -> cbv_stack_term { tab; infos = old_info; sigma } TOP (subs_id 0) c) - flgs - env - (Reductionops.safe_evar_value sigma) in - { tab = CClosure.create_tab (); infos; sigma } +let create_cbv_infos reds env sigma = + { tab = KeyTable.create 91; reds; env; sigma } diff --git a/pretyping/classops.ml b/pretyping/classops.ml index b026397abf..73141191cf 100644 --- a/pretyping/classops.ml +++ b/pretyping/classops.ml @@ -15,7 +15,6 @@ open Names open Constr open Libnames open Globnames -open Nametab open Libobject open Mod_subst @@ -228,14 +227,14 @@ let string_of_class = function | CL_FUN -> "Funclass" | CL_SORT -> "Sortclass" | CL_CONST sp -> - string_of_qualid (shortest_qualid_of_global Id.Set.empty (ConstRef sp)) + string_of_qualid (Nametab.shortest_qualid_of_global Id.Set.empty (ConstRef sp)) | CL_PROJ sp -> let sp = Projection.Repr.constant sp in - string_of_qualid (shortest_qualid_of_global Id.Set.empty (ConstRef sp)) + string_of_qualid (Nametab.shortest_qualid_of_global Id.Set.empty (ConstRef sp)) | CL_IND sp -> - string_of_qualid (shortest_qualid_of_global Id.Set.empty (IndRef sp)) + string_of_qualid (Nametab.shortest_qualid_of_global Id.Set.empty (IndRef sp)) | CL_SECVAR sp -> - string_of_qualid (shortest_qualid_of_global Id.Set.empty (VarRef sp)) + string_of_qualid (Nametab.shortest_qualid_of_global Id.Set.empty (VarRef sp)) let pr_class x = str (string_of_class x) @@ -520,7 +519,7 @@ module CoercionPrinting = let compare = GlobRef.Ordered.compare let encode = coercion_of_reference let subst = subst_coe_typ - let printer x = pr_global_env Id.Set.empty x + let printer x = Nametab.pr_global_env Id.Set.empty x let key = ["Printing";"Coercion"] let title = "Explicitly printed coercions: " let member_message x b = diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 592057ab41..072ac9deed 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -25,7 +25,6 @@ open Termops open Namegen open Libnames open Globnames -open Nametab open Mod_subst open Decl_kinds open Context.Named.Declaration @@ -58,7 +57,7 @@ let add_name_opt na b t (nenv, env) = (* Tools for printing of Cases *) let encode_inductive r = - let indsp = global_inductive r in + let indsp = Nametab.global_inductive r in let constr_lengths = constructors_nrealargs indsp in (indsp,constr_lengths) @@ -97,7 +96,7 @@ module PrintingInductiveMake = let compare = ind_ord let encode = Test.encode let subst subst obj = subst_ind subst obj - let printer ind = pr_global_env Id.Set.empty (IndRef ind) + let printer ind = Nametab.pr_global_env Id.Set.empty (IndRef ind) let key = ["Printing";Test.field] let title = Test.title let member_message x = Test.member_message (printer x) diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml index e49ba75b3f..89f64d328a 100644 --- a/pretyping/indrec.ml +++ b/pretyping/indrec.ml @@ -29,7 +29,6 @@ open Inductive open Inductiveops open Environ open Reductionops -open Nametab open Context.Rel.Declaration type dep_flag = bool @@ -618,6 +617,6 @@ let lookup_eliminator ind_sp s = user_err ~hdr:"default_elim" (strbrk "Cannot find the elimination combinator " ++ Id.print id ++ strbrk ", the elimination of the inductive definition " ++ - pr_global_env Id.Set.empty (IndRef ind_sp) ++ + Nametab.pr_global_env Id.Set.empty (IndRef ind_sp) ++ strbrk " on sort " ++ Termops.pr_sort_family s ++ strbrk " is probably not allowed.") diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml index f8dc5ba4d6..5d74b59b27 100644 --- a/pretyping/recordops.ml +++ b/pretyping/recordops.ml @@ -20,7 +20,6 @@ open Util open Pp open Names open Globnames -open Nametab open Constr open Libobject open Mod_subst @@ -330,7 +329,7 @@ let add_canonical_structure x = Lib.add_anonymous_leaf (inCanonStruc x) let error_not_structure ref description = user_err ~hdr:"object_declare" (str"Could not declare a canonical structure " ++ - (Id.print (basename_of_global ref) ++ str"." ++ spc() ++ + (Id.print (Nametab.basename_of_global ref) ++ str"." ++ spc() ++ description)) let check_and_decompose_canonical_structure ref = diff --git a/printing/printer.ml b/printing/printer.ml index 990bdaad7d..3cf995a005 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -15,7 +15,6 @@ open Names open Constr open Environ open Globnames -open Nametab open Evd open Refiner open Constrextern @@ -242,7 +241,7 @@ let pr_abstract_cumulativity_info sigma cumi = (**********************************************************************) (* Global references *) -let pr_global_env = pr_global_env +let pr_global_env = Nametab.pr_global_env let pr_global = pr_global_env Id.Set.empty let pr_universe_instance evd inst = diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index 5d1faf1465..388bf8efb5 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -68,7 +68,10 @@ let pf_ids_set_of_hyps gls = let pf_get_new_id id gls = next_ident_away id (pf_ids_set_of_hyps gls) -let pf_global gls id = EConstr.of_constr (UnivGen.constr_of_global (Constrintern.construct_reference (pf_hyps gls) id)) +let pf_global gls id = + let env = pf_env gls in + let sigma = project gls in + Evd.fresh_global env sigma (Constrintern.construct_reference (pf_hyps gls) id) let pf_reduction_of_red_expr gls re c = let (redfun, _) = reduction_of_red_expr (pf_env gls) re in diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli index 3432ad4afa..f302960870 100644 --- a/proofs/tacmach.mli +++ b/proofs/tacmach.mli @@ -34,7 +34,7 @@ val pf_hyps_types : goal sigma -> (Id.t * types) list val pf_nth_hyp_id : goal sigma -> int -> Id.t val pf_last_hyp : goal sigma -> named_declaration val pf_ids_of_hyps : goal sigma -> Id.t list -val pf_global : goal sigma -> Id.t -> constr +val pf_global : goal sigma -> Id.t -> evar_map * constr val pf_unsafe_type_of : goal sigma -> constr -> types val pf_type_of : goal sigma -> constr -> evar_map * types val pf_hnf_type_of : goal sigma -> constr -> types diff --git a/test-suite/bugs/closed/bug_8785.v b/test-suite/bugs/closed/bug_8785.v new file mode 100644 index 0000000000..b10569499e --- /dev/null +++ b/test-suite/bugs/closed/bug_8785.v @@ -0,0 +1,44 @@ +Universe u v w. +Inductive invertible {X:Type@{u}} {Y:Type} (f:X->Y) : Prop := . + +Inductive FiniteT : Type -> Prop := + | add_finite: forall T:Type@{v}, FiniteT T -> FiniteT (option T) + | bij_finite: forall (X:Type@{w}) (Y:Type) (f:X->Y), FiniteT X -> + invertible f -> FiniteT Y. + +Set Printing Universes. + +Axiom a : False. +(* +Constraint v <= u. +Constraint v <= w. +*) +Lemma finite_subtype: forall (X:Type) (P:X->Prop), + FiniteT X -> (forall x:X, P x \/ ~ P x) -> + FiniteT {x:X | P x}. +Proof. +intros. +induction H. + +destruct (H0 None). +elim a. + +pose (g := fun (x:{x:T | P (Some x)}) => + match x return {x:option T | P x} with + | exist _ x0 i => exist (fun x:option T => P x) (Some x0) i + end). +apply bij_finite with _ g. +apply IHFiniteT. +intro; apply H0. +elim a. + +pose (g := fun (x:{x:X | P (f x)}) => + match x with + | exist _ x0 i => exist (fun x:Y => P x) (f x0) i + end). +apply bij_finite with _ g. +apply IHFiniteT. +intro; apply H0. +elim a. + +Qed. diff --git a/test-suite/bugs/closed/bug_8794.v b/test-suite/bugs/closed/bug_8794.v new file mode 100644 index 0000000000..5ff0b30260 --- /dev/null +++ b/test-suite/bugs/closed/bug_8794.v @@ -0,0 +1,11 @@ +(* This used to raise an anomaly in 8.8 *) + +Inductive T := Tau (t : T). + +Notation idT t := (match t with Tau t => Tau t end). + +Lemma match_itree : forall (t : T), t = idT t. +Proof. destruct t; auto. Qed. + +Lemma what (k : unit -> T) : k tt = k tt. +Proof. rewrite match_itree. Abort. diff --git a/theories/Strings/ByteVector.v b/theories/Strings/ByteVector.v new file mode 100644 index 0000000000..16f26002d2 --- /dev/null +++ b/theories/Strings/ByteVector.v @@ -0,0 +1,56 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +Require Import Ascii Basics Bvector Psatz String Vector. +Export VectorNotations. +Open Scope program_scope. +Open Scope string_scope. + +Definition ByteVector := Vector.t ascii. + +Definition ByteNil : ByteVector 0 := Vector.nil ascii. + +Definition little_endian_to_string {n : nat} (v : ByteVector n) : string := + fold_right String v "". + +Definition to_string {n : nat} : ByteVector n -> string := + little_endian_to_string ∘ rev. + +Fixpoint little_endian_of_string (s : string) : ByteVector (length s) := + match s with + | "" => ByteNil + | String b s' => b :: little_endian_of_string s' + end. + +Definition of_string (s : string) : ByteVector (length s) := + rev (little_endian_of_string s). + +Fixpoint to_Bvector {n : nat} (v : ByteVector n) : Bvector (n * 8) := + match v with + | [] => [] + | Ascii b0 b1 b2 b3 b4 b5 b6 b7::v' => + b0::b1::b2::b3::b4::b5::b6::b7::to_Bvector v' + end. + +Fixpoint of_Bvector {n : nat} : Bvector (n * 8) -> ByteVector n := + match n with + | 0 => fun _ => [] + | S n' => + fun v => + let (b0, v1) := uncons v in + let (b1, v2) := uncons v1 in + let (b2, v3) := uncons v2 in + let (b3, v4) := uncons v3 in + let (b4, v5) := uncons v4 in + let (b5, v6) := uncons v5 in + let (b6, v7) := uncons v6 in + let (b7, v8) := uncons v7 in + Ascii b0 b1 b2 b3 b4 b5 b6 b7::of_Bvector v8 + end. diff --git a/theories/Vectors/VectorDef.v b/theories/Vectors/VectorDef.v index 390ca78c0e..4a2bddf35c 100644 --- a/theories/Vectors/VectorDef.v +++ b/theories/Vectors/VectorDef.v @@ -132,6 +132,9 @@ replace v (Fin.of_nat_lt H). Definition tl {A} := @caseS _ (fun n v => t A n) (fun h n t => t). Global Arguments tl {A} {n} v. +(** Destruct a non empty vector *) +Definition uncons {A} {n : nat} (v : t A (S n)) : A * t A n := (hd v, tl v). + (** Remove last element of a non-empty vector *) Definition shiftout {A} := @rectS _ (fun n _ => t A n) (fun a => []) (fun h _ _ H => h :: H). diff --git a/vernac/assumptions.ml b/vernac/assumptions.ml index 15c0278f47..6beac2032d 100644 --- a/vernac/assumptions.ml +++ b/vernac/assumptions.ml @@ -162,27 +162,6 @@ let label_of = function | ConstructRef ((kn,_),_) -> MutInd.label kn | VarRef id -> Label.of_id id -let fold_constr_with_full_binders g f n acc c = - let open Context.Rel.Declaration in - match Constr.kind c with - | Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _ | Construct _ -> acc - | Cast (c,_, t) -> f n (f n acc c) t - | Prod (na,t,c) -> f (g (LocalAssum (na,t)) n) (f n acc t) c - | Lambda (na,t,c) -> f (g (LocalAssum (na,t)) n) (f n acc t) c - | LetIn (na,b,t,c) -> f (g (LocalDef (na,b,t)) n) (f n (f n acc b) t) c - | App (c,l) -> Array.fold_left (f n) (f n acc c) l - | Proj (p,c) -> f n acc c - | Evar (_,l) -> Array.fold_left (f n) acc l - | Case (_,p,c,bl) -> Array.fold_left (f n) (f n (f n acc p) c) bl - | Fix (_,(lna,tl,bl)) -> - let n' = CArray.fold_left2 (fun c n t -> g (LocalAssum (n,t)) c) n lna tl in - let fd = Array.map2 (fun t b -> (t,b)) tl bl in - Array.fold_left (fun acc (t,b) -> f n' (f n acc t) b) acc fd - | CoFix (_,(lna,tl,bl)) -> - let n' = CArray.fold_left2 (fun c n t -> g (LocalAssum (n,t)) c) n lna tl in - let fd = Array.map2 (fun t b -> (t,b)) tl bl in - Array.fold_left (fun acc (t,b) -> f n' (f n acc t) b) acc fd - let rec traverse current ctx accu t = match Constr.kind t with | Var id -> let body () = id |> Global.lookup_named |> NamedDecl.get_value in @@ -205,10 +184,10 @@ let rec traverse current ctx accu t = match Constr.kind t with traverse_object ~inhabits:(current,ctx,Vars.subst1 mkProp oty) accu body (ConstRef kn) | _ -> - fold_constr_with_full_binders + Constr.fold_with_full_binders Context.Rel.add (traverse current) ctx accu t end -| _ -> fold_constr_with_full_binders +| _ -> Constr.fold_with_full_binders Context.Rel.add (traverse current) ctx accu t and traverse_object ?inhabits (curr, data, ax2ty) body obj = diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml index 148d4437fa..9f71def8fc 100644 --- a/vernac/auto_ind_decl.ml +++ b/vernac/auto_ind_decl.ml @@ -63,20 +63,20 @@ exception ConstructorWithNonParametricInductiveType of inductive exception DecidabilityIndicesNotSupported (* Some pre declaration of constant we are going to use *) -let andb_prop = fun _ -> UnivGen.constr_of_global (Coqlib.lib_ref "core.bool.andb_prop") +let andb_prop = fun _ -> UnivGen.constr_of_monomorphic_global (Coqlib.lib_ref "core.bool.andb_prop") let andb_true_intro = fun _ -> - UnivGen.constr_of_global + UnivGen.constr_of_monomorphic_global (Coqlib.lib_ref "core.bool.andb_true_intro") (* We avoid to use lazy as the binding of constants can change *) -let bb () = UnivGen.constr_of_global (Coqlib.lib_ref "core.bool.type") -let tt () = UnivGen.constr_of_global (Coqlib.lib_ref "core.bool.true") -let ff () = UnivGen.constr_of_global (Coqlib.lib_ref "core.bool.false") -let eq () = UnivGen.constr_of_global (Coqlib.lib_ref "core.eq.type") +let bb () = UnivGen.constr_of_monomorphic_global (Coqlib.lib_ref "core.bool.type") +let tt () = UnivGen.constr_of_monomorphic_global (Coqlib.lib_ref "core.bool.true") +let ff () = UnivGen.constr_of_monomorphic_global (Coqlib.lib_ref "core.bool.false") +let eq () = UnivGen.constr_of_monomorphic_global (Coqlib.lib_ref "core.eq.type") -let sumbool () = UnivGen.constr_of_global (Coqlib.lib_ref "core.sumbool.type") -let andb = fun _ -> UnivGen.constr_of_global (Coqlib.lib_ref "core.bool.andb") +let sumbool () = UnivGen.constr_of_monomorphic_global (Coqlib.lib_ref "core.sumbool.type") +let andb = fun _ -> UnivGen.constr_of_monomorphic_global (Coqlib.lib_ref "core.bool.andb") let induct_on c = induction false None c None None let destruct_on c = destruct false None c None None @@ -873,7 +873,7 @@ let compute_dec_goal ind lnamesparrec nparrec = create_input ( mkNamedProd n (mkFullInd ind (2*nparrec)) ( mkNamedProd m (mkFullInd ind (2*nparrec+1)) ( - mkApp(sumbool(),[|eqnm;mkApp (UnivGen.constr_of_global @@ Coqlib.lib_ref "core.not.type",[|eqnm|])|]) + mkApp(sumbool(),[|eqnm;mkApp (UnivGen.constr_of_monomorphic_global @@ Coqlib.lib_ref "core.not.type",[|eqnm|])|]) ) ) ) diff --git a/vernac/class.ml b/vernac/class.ml index 614b2181d9..526acd40b5 100644 --- a/vernac/class.ml +++ b/vernac/class.ml @@ -21,7 +21,6 @@ open Environ open Classops open Declare open Globnames -open Nametab open Decl_kinds let strength_min l = if List.mem `LOCAL l then `LOCAL else `GLOBAL @@ -310,7 +309,7 @@ let add_coercion_hook poly local ref = | Global -> false in let () = try_add_new_coercion ref ~local poly in - let msg = pr_global_env Id.Set.empty ref ++ str " is now a coercion" in + let msg = Nametab.pr_global_env Id.Set.empty ref ++ str " is now a coercion" in Flags.if_verbose Feedback.msg_info msg let add_coercion_hook poly = Lemmas.mk_hook (add_coercion_hook poly) diff --git a/vernac/classes.ml b/vernac/classes.ml index 3cf5e9bfdf..52c1e1cf98 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -12,7 +12,6 @@ module CVars = Vars open Names open EConstr -open Nametab open CErrors open Util open Typeclasses_errors @@ -67,7 +66,7 @@ let intern_info {hint_priority;hint_pattern} = (** TODO: add subinstances *) let existing_instance glob g info = - let c = global g in + let c = Nametab.global g in let info = Option.default Hints.empty_hint_info info in let info = intern_info info in let instance, _ = Global.type_of_global_in_context (Global.env ()) c in diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml index 7b28895814..885a22b209 100644 --- a/vernac/comInductive.ml +++ b/vernac/comInductive.ml @@ -22,7 +22,6 @@ open Nameops open Constrexpr open Constrexpr_ops open Constrintern -open Nametab open Impargs open Reductionops open Indtypes @@ -575,6 +574,6 @@ let do_mutual_inductive ~template udecl indl cum poly prv ~uniform finite = (* Declare the possible notations of inductive types *) List.iter (Metasyntax.add_notation_interpretation (Global.env ())) ntns; (* Declare the coercions *) - List.iter (fun qid -> Class.try_add_new_coercion (locate qid) ~local:false poly) coes; + List.iter (fun qid -> Class.try_add_new_coercion (Nametab.locate qid) ~local:false poly) coes; (* If positivity is assumed declares itself as unsafe. *) if Environ.deactivated_guard (Global.env ()) then Feedback.feedback Feedback.AddedAxiom else () diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml index 5f2818c12b..4efbb968fb 100644 --- a/vernac/indschemes.ml +++ b/vernac/indschemes.ml @@ -33,7 +33,6 @@ open Globnames open Goptions open Nameops open Termops -open Nametab open Smartlocate open Vernacexpr open Ind_tables @@ -369,7 +368,7 @@ requested | InSet -> recs ^ "_nodep" | InType -> recs ^ "t_nodep") ) in - let newid = add_suffix (basename_of_global (IndRef ind)) suffix in + let newid = add_suffix (Nametab.basename_of_global (IndRef ind)) suffix in let newref = CAst.make newid in ((newref,isdep,ind,z)::l1),l2 in diff --git a/vernac/obligations.ml b/vernac/obligations.ml index 0ac97a74e4..fbf552e649 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -266,7 +266,7 @@ let eterm_obligations env name evm fs ?status t ty = let hide_obligation () = Coqlib.check_required_library ["Coq";"Program";"Tactics"]; - UnivGen.constr_of_global (Coqlib.lib_ref "program.tactics.obligation") + UnivGen.constr_of_monomorphic_global (Coqlib.lib_ref "program.tactics.obligation") let pperror cmd = CErrors.user_err ~hdr:"Program" cmd let error s = pperror (str s) diff --git a/vernac/search.ml b/vernac/search.ml index 04dcb7d565..2273130668 100644 --- a/vernac/search.ml +++ b/vernac/search.ml @@ -18,7 +18,6 @@ open Environ open Pattern open Libnames open Globnames -open Nametab module NamedDecl = Context.Named.Declaration @@ -192,7 +191,7 @@ let rec head_filter pat ref env sigma typ = | _ -> false let full_name_of_reference ref = - let (dir,id) = repr_path (path_of_global ref) in + let (dir,id) = repr_path (Nametab.path_of_global ref) in DirPath.to_string dir ^ "." ^ Id.to_string id (** Whether a reference is blacklisted *) @@ -204,14 +203,14 @@ let blacklist_filter_aux () = List.for_all is_not_bl l let module_filter (mods, outside) ref env typ = - let sp = path_of_global ref in + let sp = Nametab.path_of_global ref in let sl = dirpath sp in let is_outside md = not (is_dirpath_prefix_of md sl) in let is_inside md = is_dirpath_prefix_of md sl in if outside then List.for_all is_outside mods else List.is_empty mods || List.exists is_inside mods -let name_of_reference ref = Id.to_string (basename_of_global ref) +let name_of_reference ref = Id.to_string (Nametab.basename_of_global ref) let search_about_filter query gr env typ = match query with | GlobSearchSubPattern pat -> |