aboutsummaryrefslogtreecommitdiff
path: root/vernac
diff options
context:
space:
mode:
Diffstat (limited to 'vernac')
-rw-r--r--vernac/assumptions.ml25
-rw-r--r--vernac/auto_ind_decl.ml18
-rw-r--r--vernac/class.ml3
-rw-r--r--vernac/classes.ml3
-rw-r--r--vernac/comInductive.ml3
-rw-r--r--vernac/indschemes.ml3
-rw-r--r--vernac/obligations.ml2
-rw-r--r--vernac/search.ml7
8 files changed, 19 insertions, 45 deletions
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 ->
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-04 02:47:48 +0000