aboutsummaryrefslogtreecommitdiff
path: root/vernac
diff options
context:
space:
mode:
Diffstat (limited to 'vernac')
-rw-r--r--vernac/assumptions.ml14
-rw-r--r--vernac/auto_ind_decl.ml7
-rw-r--r--vernac/class.ml25
-rw-r--r--vernac/classes.ml18
-rw-r--r--vernac/comAssumption.ml7
-rw-r--r--vernac/comInductive.ml11
-rw-r--r--vernac/comProgramFixpoint.ml3
-rw-r--r--vernac/declareDef.ml5
-rw-r--r--vernac/indschemes.ml11
-rw-r--r--vernac/lemmas.ml23
-rw-r--r--vernac/record.ml25
-rw-r--r--vernac/search.ml11
-rw-r--r--vernac/vernacentries.ml20
13 files changed, 87 insertions, 93 deletions
diff --git a/vernac/assumptions.ml b/vernac/assumptions.ml
index d7cb9dc727..ab341e4ab8 100644
--- a/vernac/assumptions.ml
+++ b/vernac/assumptions.ml
@@ -24,7 +24,6 @@ open Constr
open Context
open Declarations
open Mod_subst
-open Globnames
open Printer
open Context.Named.Declaration
@@ -157,13 +156,15 @@ let lookup_mind mind =
(** Graph traversal of an object, collecting on the way the dependencies of
traversed objects *)
-let label_of = function
+let label_of = let open GlobRef in function
| ConstRef kn -> Constant.label kn
| IndRef (kn,_)
| ConstructRef ((kn,_),_) -> MutInd.label kn
| VarRef id -> Label.of_id id
-let rec traverse current ctx accu t = match Constr.kind t with
+let rec traverse current ctx accu t =
+ let open GlobRef in
+ match Constr.kind t with
| Var id ->
let body () = id |> Global.lookup_named |> NamedDecl.get_value in
traverse_object accu body (VarRef id)
@@ -218,7 +219,7 @@ and traverse_object ?inhabits (curr, data, ax2ty) body obj =
definition share exactly the same dependencies. Also, there is no explicit
dependency between mutually defined inductives and constructors. *)
and traverse_inductive (curr, data, ax2ty) mind obj =
- let firstind_ref = (IndRef (mind, 0)) in
+ let firstind_ref = (GlobRef.IndRef (mind, 0)) in
let label = label_of obj in
let data, ax2ty =
(* Invariant : I_0 \in data iff I_i \in data iff c_ij \in data
@@ -264,9 +265,9 @@ and traverse_inductive (curr, data, ax2ty) mind obj =
(* Maps all these dependencies to inductives and constructors*)
let data = Array.fold_left_i (fun n data oib ->
let ind = (mind, n) in
- let data = GlobRef.Map_env.add (IndRef ind) contents data in
+ let data = GlobRef.Map_env.add (GlobRef.IndRef ind) contents data in
Array.fold_left_i (fun k data _ ->
- GlobRef.Map_env.add (ConstructRef (ind, k+1)) contents data
+ GlobRef.Map_env.add (GlobRef.ConstructRef (ind, k+1)) contents data
) data oib.mind_consnames) data mib.mind_packets
in
data, ax2ty
@@ -298,6 +299,7 @@ let type_of_constant cb = cb.Declarations.const_type
let assumptions ?(add_opaque=false) ?(add_transparent=false) st gr t =
(* Only keep the transitive dependencies *)
let (_, graph, ax2ty) = traverse (label_of gr) t in
+ let open GlobRef in
let fold obj _ accu = match obj with
| VarRef id ->
let decl = Global.lookup_named id in
diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml
index 9b96fbf68a..d414d57c0d 100644
--- a/vernac/auto_ind_decl.ml
+++ b/vernac/auto_ind_decl.ml
@@ -21,7 +21,6 @@ open Vars
open Termops
open Declarations
open Names
-open Globnames
open Inductiveops
open Tactics
open Ind_tables
@@ -201,7 +200,7 @@ let build_beq_scheme mode kn =
let eid = Id.of_string ("eq_"^(Id.to_string x)) in
let () =
try ignore (Environ.lookup_named eid env)
- with Not_found -> raise (ParameterWithoutEquality (VarRef x))
+ with Not_found -> raise (ParameterWithoutEquality (GlobRef.VarRef x))
in
mkVar eid, Evd.empty_side_effects
| Cast (x,_,_) -> aux (Term.applist (x,a))
@@ -240,7 +239,7 @@ let build_beq_scheme mode kn =
try let _ = Environ.constant_opt_value_in env (kneq, u) in
Term.applist (mkConst kneq,a),
Evd.empty_side_effects
- with Not_found -> raise (ParameterWithoutEquality (ConstRef kn)))
+ with Not_found -> raise (ParameterWithoutEquality (GlobRef.ConstRef kn)))
| Proj _ -> raise (EqUnknown "projection")
| Construct _ -> raise (EqUnknown "constructor")
| Case _ -> raise (EqUnknown "match")
@@ -655,7 +654,7 @@ repeat ( apply andb_prop in z;let z1:= fresh "Z" in destruct z as [z1 z]).
| App (c,ca) -> (
match EConstr.kind sigma c with
| Ind (indeq, u) ->
- if GlobRef.equal (IndRef indeq) Coqlib.(lib_ref "core.eq.type")
+ if GlobRef.equal (GlobRef.IndRef indeq) Coqlib.(lib_ref "core.eq.type")
then
Tacticals.New.tclTHEN
(do_replace_bl mode bl_scheme_key ind
diff --git a/vernac/class.ml b/vernac/class.ml
index f79e459f43..766625a21a 100644
--- a/vernac/class.ml
+++ b/vernac/class.ml
@@ -20,7 +20,6 @@ open Termops
open Environ
open Classops
open Declare
-open Globnames
open Libobject
let strength_min l = if List.mem `LOCAL l then `LOCAL else `GLOBAL
@@ -71,10 +70,10 @@ let check_reference_arity ref =
let check_arity = function
| CL_FUN | CL_SORT -> ()
- | CL_CONST cst -> check_reference_arity (ConstRef cst)
- | CL_PROJ p -> check_reference_arity (ConstRef (Projection.Repr.constant p))
- | CL_SECVAR id -> check_reference_arity (VarRef id)
- | CL_IND kn -> check_reference_arity (IndRef kn)
+ | CL_CONST cst -> check_reference_arity (GlobRef.ConstRef cst)
+ | CL_PROJ p -> check_reference_arity (GlobRef.ConstRef (Projection.Repr.constant p))
+ | CL_SECVAR id -> check_reference_arity (GlobRef.VarRef id)
+ | CL_IND kn -> check_reference_arity (GlobRef.IndRef kn)
(* Coercions *)
@@ -90,12 +89,12 @@ let uniform_cond sigma ctx lt =
lt (Context.Rel.to_extended_list EConstr.mkRel 0 ctx)
let class_of_global = function
- | ConstRef sp ->
+ | GlobRef.ConstRef sp ->
(match Recordops.find_primitive_projection sp with
| Some p -> CL_PROJ p | None -> CL_CONST sp)
- | IndRef sp -> CL_IND sp
- | VarRef id -> CL_SECVAR id
- | ConstructRef _ as c ->
+ | GlobRef.IndRef sp -> CL_IND sp
+ | GlobRef.VarRef id -> CL_SECVAR id
+ | GlobRef.ConstructRef _ as c ->
user_err ~hdr:"class_of_global"
(str "Constructors, such as " ++ Printer.pr_global c ++
str ", cannot be used as a class.")
@@ -152,7 +151,7 @@ let strength_of_cl = function
| _ -> `GLOBAL
let strength_of_global = function
- | VarRef _ -> `LOCAL
+ | GlobRef.VarRef _ -> `LOCAL
| _ -> `GLOBAL
let get_strength stre ref cls clt =
@@ -179,7 +178,7 @@ let build_id_coercion idf_opt source poly =
let env = Global.env () in
let sigma = Evd.from_env env in
let sigma, vs = match source with
- | CL_CONST sp -> Evd.fresh_global env sigma (ConstRef sp)
+ | CL_CONST sp -> Evd.fresh_global env sigma (GlobRef.ConstRef sp)
| _ -> error_not_transparent source in
let vs = EConstr.Unsafe.to_constr vs in
let c = match constant_opt_value_in env (destConst vs) with
@@ -223,7 +222,7 @@ let build_id_coercion idf_opt source poly =
in
let kind = Decls.(IsDefinition IdentityCoercion) in
let kn = declare_constant ~name ~kind constr_entry in
- ConstRef kn
+ GlobRef.ConstRef kn
let check_source = function
| Some (CL_FUN as s) -> raise (CoercionError (ForbiddenSourceClass s))
@@ -267,7 +266,7 @@ let inCoercion : coercion -> obj =
let declare_coercion coef ?(local = false) ~isid ~src:cls ~target:clt ~params:ps =
let isproj =
match coef with
- | ConstRef c -> Recordops.find_primitive_projection c
+ | GlobRef.ConstRef c -> Recordops.find_primitive_projection c
| _ -> None
in
let c = {
diff --git a/vernac/classes.ml b/vernac/classes.ml
index 24f4f7fe70..efe452d5f1 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -193,6 +193,7 @@ let discharge_class (_,cl) =
ctx
in
let abs_context cl =
+ let open GlobRef in
match cl.cl_impl with
| VarRef _ | ConstructRef _ -> assert false
| ConstRef cst -> Lib.section_segment_of_constant cst
@@ -255,7 +256,7 @@ let add_class env sigma cl =
| Some (Backward, info) ->
(match body with
| None -> CErrors.user_err Pp.(str "Non-definable projection can not be declared as a subinstance")
- | Some b -> declare_instance ~warn:true env sigma (Some info) false (ConstRef b))
+ | Some b -> declare_instance ~warn:true env sigma (Some info) false (GlobRef.ConstRef b))
| _ -> ())
cl.cl_projs
@@ -298,6 +299,7 @@ let type_ctx_instance ~program_mode env sigma ctx inst subst =
in aux (sigma, subst, []) inst (List.rev ctx)
let id_of_class cl =
+ let open GlobRef in
match cl.cl_impl with
| ConstRef kn -> Label.to_id @@ Constant.label kn
| IndRef (kn,i) ->
@@ -325,8 +327,8 @@ let declare_instance_constant info global imps ?hook name decl poly sigma term t
let entry = Declare.definition_entry ~types:termtype ~univs:uctx term in
let kn = Declare.declare_constant ~name ~kind (Declare.DefinitionEntry entry) in
Declare.definition_message name;
- Declare.declare_univ_binders (ConstRef kn) (Evd.universe_binders sigma);
- instance_hook info global imps ?hook (ConstRef kn)
+ Declare.declare_univ_binders (GlobRef.ConstRef kn) (Evd.universe_binders sigma);
+ instance_hook info global imps ?hook (GlobRef.ConstRef kn)
let do_declare_instance sigma ~global ~poly k u ctx ctx' pri decl imps subst name =
let subst = List.fold_left2
@@ -338,17 +340,17 @@ let do_declare_instance sigma ~global ~poly k u ctx ctx' pri decl imps subst nam
let sigma, entry = DeclareDef.prepare_parameter ~allow_evars:false ~poly sigma decl termtype in
let cst = Declare.declare_constant ~name
~kind:Decls.(IsAssumption Logical) (Declare.ParameterEntry entry) in
- Declare.declare_univ_binders (ConstRef cst) (Evd.universe_binders sigma);
- instance_hook pri global imps (ConstRef cst)
+ Declare.declare_univ_binders (GlobRef.ConstRef cst) (Evd.universe_binders sigma);
+ instance_hook pri global imps (GlobRef.ConstRef cst)
let declare_instance_program env sigma ~global ~poly id pri imps decl term termtype =
let hook { DeclareDef.Hook.S.scope; dref; _ } =
- let cst = match dref with ConstRef kn -> kn | _ -> assert false in
+ let cst = match dref with GlobRef.ConstRef kn -> kn | _ -> assert false in
Impargs.declare_manual_implicits false dref imps;
let pri = intern_info pri in
let env = Global.env () in
let sigma = Evd.from_env env in
- declare_instance env sigma (Some pri) (not global) (ConstRef cst)
+ declare_instance env sigma (Some pri) (not global) (GlobRef.ConstRef cst)
in
let obls, constr, typ =
match term with
@@ -440,7 +442,7 @@ let do_instance_type_ctx_instance props k env' ctx' sigma ~program_mode subst =
let {CAst.loc;v=mid} = get_id loc_mid in
List.iter (fun (n, _, x) ->
if Name.equal n (Name mid) then
- Option.iter (fun x -> Dumpglob.add_glob ?loc (ConstRef x)) x) k.cl_projs;
+ Option.iter (fun x -> Dumpglob.add_glob ?loc (GlobRef.ConstRef x)) x) k.cl_projs;
c :: props, rest'
with Not_found ->
((CAst.make @@ CHole (None(* Some Evar_kinds.GoalEvar *), Namegen.IntroAnonymous, None)) :: props), rest
diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml
index c561d4a2a4..d59d471d5f 100644
--- a/vernac/comAssumption.ml
+++ b/vernac/comAssumption.ml
@@ -14,7 +14,6 @@ open Vars
open Declare
open Names
open Context
-open Globnames
open Constrexpr_ops
open Constrintern
open Impargs
@@ -54,7 +53,7 @@ match scope with
let decl = SectionLocalAssum {typ; univs; poly; impl} in
let () = declare_variable ~name ~kind decl in
let () = assumption_message name in
- let r = VarRef name in
+ let r = GlobRef.VarRef name in
let () = maybe_declare_manual_implicits true r imps in
let env = Global.env () in
let sigma = Evd.from_env env in
@@ -72,7 +71,7 @@ match scope with
let kind = Decls.IsAssumption kind in
let decl = Declare.ParameterEntry (None,(typ,univs),inl) in
let kn = declare_constant ~name ~local ~kind decl in
- let gr = ConstRef kn in
+ let gr = GlobRef.ConstRef kn in
let () = maybe_declare_manual_implicits false gr imps in
let () = Declare.declare_univ_binders gr pl in
let () = assumption_message name in
@@ -285,7 +284,7 @@ let context ~poly l =
in
let cst = Declare.declare_constant ~name ~kind decl in
let env = Global.env () in
- Classes.declare_instance env sigma (Some Hints.empty_hint_info) true (ConstRef cst);
+ Classes.declare_instance env sigma (Some Hints.empty_hint_info) true (GlobRef.ConstRef cst);
status
else
let test x = match x.CAst.v with
diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml
index d99d3e65fd..65db4401d9 100644
--- a/vernac/comInductive.ml
+++ b/vernac/comInductive.ml
@@ -18,7 +18,6 @@ open Environ
open Declare
open Names
open Libnames
-open Globnames
open Nameops
open Constrexpr
open Constrexpr_ops
@@ -522,7 +521,7 @@ let is_recursive mie =
let warn_non_primitive_record =
CWarnings.create ~name:"non-primitive-record" ~category:"record"
(fun indsp ->
- (hov 0 (str "The record " ++ Nametab.pr_global_env Id.Set.empty (IndRef indsp) ++
+ (hov 0 (str "The record " ++ Nametab.pr_global_env Id.Set.empty (GlobRef.IndRef indsp) ++
strbrk" could not be defined as a primitive record")))
let declare_mutual_inductive_with_eliminations ?(primitive_expected=false) mie pl impls =
@@ -540,15 +539,15 @@ let declare_mutual_inductive_with_eliminations ?(primitive_expected=false) mie p
let (_, kn), prim = declare_mind mie in
let mind = Global.mind_of_delta_kn kn in
if primitive_expected && not prim then warn_non_primitive_record (mind,0);
- Declare.declare_univ_binders (IndRef (mind,0)) pl;
+ Declare.declare_univ_binders (GlobRef.IndRef (mind,0)) pl;
List.iteri (fun i (indimpls, constrimpls) ->
let ind = (mind,i) in
- let gr = IndRef ind in
+ let gr = GlobRef.IndRef ind in
maybe_declare_manual_implicits false gr indimpls;
List.iteri
(fun j impls ->
maybe_declare_manual_implicits false
- (ConstructRef (ind, succ j)) impls)
+ (GlobRef.ConstructRef (ind, succ j)) impls)
constrimpls)
impls;
Flags.if_verbose Feedback.msg_info (minductive_message names);
@@ -614,6 +613,6 @@ let make_cases ind =
let n' = Namegen.next_name_away_with_default (Id.to_string Namegen.default_dependent_ident) n.Context.binder_name avoid in
Id.to_string n' :: rename (Id.Set.add n' avoid) l in
let al' = rename Id.Set.empty al in
- let consref = ConstructRef (ith_constructor_of_inductive ind (i + 1)) in
+ let consref = GlobRef.ConstructRef (ith_constructor_of_inductive ind (i + 1)) in
(Libnames.string_of_qualid (Nametab.shortest_qualid_of_global Id.Set.empty consref) :: al') :: l)
mip.mind_nf_lc []
diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml
index 4d663d6b0e..0fd65ad9b4 100644
--- a/vernac/comProgramFixpoint.ml
+++ b/vernac/comProgramFixpoint.ml
@@ -17,7 +17,6 @@ open Vars
open Declare
open Names
open Libnames
-open Globnames
open Nameops
open Constrexpr
open Constrexpr_ops
@@ -213,7 +212,7 @@ let build_wellfounded (recname,pl,bl,arityc,body) poly r measure notation =
let ce = definition_entry ~types:ty ~univs (EConstr.to_constr sigma body) in
(* FIXME: include locality *)
let c = Declare.declare_constant ~name:recname ~kind:Decls.(IsDefinition Definition) (DefinitionEntry ce) in
- let gr = ConstRef c in
+ let gr = GlobRef.ConstRef c in
if Impargs.is_implicit_args () || not (List.is_empty impls) then
Impargs.declare_manual_implicits false gr impls
in
diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml
index 69338c0ba6..5e4f2dcd34 100644
--- a/vernac/declareDef.ml
+++ b/vernac/declareDef.ml
@@ -9,7 +9,6 @@
(************************************************************************)
open Declare
-open Globnames
open Impargs
type locality = Discharge | Global of Declare.import_status
@@ -51,10 +50,10 @@ let declare_definition ~name ~scope ~kind ?hook_data udecl ce imps =
let () =
declare_variable ~name ~kind:Decls.(IsDefinition kind) (SectionLocalDef ce)
in
- VarRef name
+ Names.GlobRef.VarRef name
| Global local ->
let kn = declare_constant ~name ~local ~kind:Decls.(IsDefinition kind) (DefinitionEntry ce) in
- let gr = ConstRef kn in
+ let gr = Names.GlobRef.ConstRef kn in
let () = Declare.declare_univ_binders gr udecl in
gr
in
diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml
index d9b839e857..23a8bf20a3 100644
--- a/vernac/indschemes.ml
+++ b/vernac/indschemes.ml
@@ -27,7 +27,6 @@ open Inductive
open Indrec
open Declare
open Libnames
-open Globnames
open Goptions
open Nameops
open Termops
@@ -376,7 +375,7 @@ requested
| InSet -> recs ^ "_nodep"
| InType -> recs ^ "t_nodep")
) in
- let newid = add_suffix (Nametab.basename_of_global (IndRef ind)) suffix in
+ let newid = add_suffix (Nametab.basename_of_global (GlobRef.IndRef ind)) suffix in
let newref = CAst.make newid in
((newref,isdep,ind,z)::l1),l2
in
@@ -394,7 +393,7 @@ let do_mutual_induction_scheme ?(force_mutual=false) lnamedepindsort =
let evd, indu, inst =
match inst with
| None ->
- let _, ctx = Typeops.type_of_global_in_context env0 (IndRef ind) in
+ let _, ctx = Typeops.type_of_global_in_context env0 (GlobRef.IndRef ind) in
let u, ctx = UnivGen.fresh_instance_from ctx None in
let evd = Evd.from_ctx (UState.of_context_set ctx) in
evd, (ind,u), Some u
@@ -408,14 +407,14 @@ let do_mutual_induction_scheme ?(force_mutual=false) lnamedepindsort =
(* NB: build_mutual_induction_scheme forces nonempty list of mutual inductives
(force_mutual is about the generated schemes) *)
let _,_,ind,_ = List.hd lnamedepindsort in
- Global.is_polymorphic (IndRef ind)
+ Global.is_polymorphic (GlobRef.IndRef ind)
in
let declare decl fi lrecref =
let decltype = Retyping.get_type_of env0 sigma (EConstr.of_constr decl) in
let decltype = EConstr.to_constr sigma decltype in
let proof_output = Future.from_val ((decl,Univ.ContextSet.empty),Evd.empty_side_effects) in
let cst = define ~poly fi sigma proof_output (Some decltype) in
- ConstRef cst :: lrecref
+ GlobRef.ConstRef cst :: lrecref
in
let _ = List.fold_right2 declare listdecl lrecnames [] in
fixpoint_message None lrecnames
@@ -542,7 +541,7 @@ let do_combined_scheme name schemes =
polymorphism of the inductive block). In that case if they want
some other polymorphism they can also manually define the
combined scheme. *)
- let poly = Global.is_polymorphic (ConstRef (List.hd csts)) in
+ let poly = Global.is_polymorphic (GlobRef.ConstRef (List.hd csts)) in
ignore (define ~poly name.v sigma proof_output (Some typ));
fixpoint_message None [name.v]
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index 00316bfadf..ecea9ae4c9 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -19,7 +19,6 @@ open Constr
open Declareops
open Entries
open Nameops
-open Globnames
open Pretyping
open Termops
open Reductionops
@@ -117,10 +116,10 @@ let by tac pf =
(* Support for mutually proved theorems *)
let retrieve_first_recthm uctx = function
- | VarRef id ->
+ | GlobRef.VarRef id ->
NamedDecl.get_value (Global.lookup_named id),
Decls.variable_opacity id
- | ConstRef cst ->
+ | GlobRef.ConstRef cst ->
let cb = Global.lookup_constant cst in
(* we get the right order somehow but surely it could be enforced in a better way *)
let uctx = UState.context uctx in
@@ -178,12 +177,12 @@ let save_remaining_recthms env sigma ~poly ~scope norm univs body opaq i { Recth
in
let c = Declare.SectionLocalAssum {typ=t_i; univs; poly; impl} in
let () = Declare.declare_variable ~name ~kind c in
- (VarRef name,impargs)
+ (GlobRef.VarRef name,impargs)
| Global local ->
let kind = Decls.(IsAssumption Conjectural) in
let decl = Declare.ParameterEntry (None,(t_i,univs),None) in
let kn = Declare.declare_constant ~name ~local ~kind decl in
- (ConstRef kn,impargs))
+ (GlobRef.ConstRef kn,impargs))
| Some body ->
let body = norm body in
let rec body_i t = match Constr.kind t with
@@ -201,11 +200,11 @@ let save_remaining_recthms env sigma ~poly ~scope norm univs body opaq i { Recth
let const = Declare.definition_entry ~types:t_i ~opaque:opaq ~univs body_i in
let c = Declare.SectionLocalDef const in
let () = Declare.declare_variable ~name ~kind c in
- (VarRef name,impargs)
+ (GlobRef.VarRef name,impargs)
| Global local ->
let const = Declare.definition_entry ~types:t_i ~univs ~opaque:opaq body_i in
let kn = Declare.declare_constant ~name ~local ~kind (Declare.DefinitionEntry const) in
- (ConstRef kn,impargs)
+ (GlobRef.ConstRef kn,impargs)
let initialize_named_context_for_proof () =
let sign = Global.named_context () in
@@ -360,9 +359,9 @@ let finish_admitted env sigma ~name ~poly ~scope pe ctx hook ~udecl impargs othe
in
let kn = Declare.declare_constant ~name ~local ~kind:Decls.(IsAssumption Conjectural) (Declare.ParameterEntry pe) in
let () = Declare.assumption_message name in
- Declare.declare_univ_binders (ConstRef kn) (UState.universe_binders ctx);
+ Declare.declare_univ_binders (GlobRef.ConstRef kn) (UState.universe_binders ctx);
(* This takes care of the implicits and hook for the current constant*)
- process_recthms ?fix_exn:None ?hook env sigma ctx ~udecl ~poly ~scope:(Global local) (ConstRef kn) impargs other_thms;
+ process_recthms ?fix_exn:None ?hook env sigma ctx ~udecl ~poly ~scope:(Global local) (GlobRef.ConstRef kn) impargs other_thms;
Feedback.feedback Feedback.AddedAxiom
let save_lemma_admitted ~(lemma : t) : unit =
@@ -420,14 +419,14 @@ let finish_proved env sigma idopt po info =
let () = if should_suggest
then Proof_using.suggest_variable (Global.env ()) name
in
- VarRef name
+ GlobRef.VarRef name
| Global local ->
let kn =
Declare.declare_constant ~name ~local ~kind (Declare.DefinitionEntry const) in
let () = if should_suggest
then Proof_using.suggest_constant (Global.env ()) kn
in
- let gr = ConstRef kn in
+ let gr = GlobRef.ConstRef kn in
Declare.declare_univ_binders gr (UState.universe_binders universes);
gr
in
@@ -496,7 +495,7 @@ let finish_proved_equations lid kind proof_obj hook i types wits sigma0 =
in
let entry, args = Abstract.shrink_entry local_context entry in
let cst = Declare.declare_constant ~name:id ~kind (Declare.DefinitionEntry entry) in
- let sigma, app = Evarutil.new_global sigma (ConstRef cst) in
+ let sigma, app = Evarutil.new_global sigma (GlobRef.ConstRef cst) in
let sigma = Evd.define ev (EConstr.applist (app, List.map EConstr.of_constr args)) sigma in
sigma, cst) sigma0
(CList.combine (List.rev !wits) types) proof_obj.Proof_global.entries
diff --git a/vernac/record.ml b/vernac/record.ml
index fe89303d33..86745212e7 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -14,7 +14,6 @@ open Term
open Sorts
open Util
open Names
-open Globnames
open Nameops
open Constr
open Context
@@ -362,10 +361,10 @@ let declare_projections indsp ctx ?(kind=Decls.StructureComponent) binder_name f
with Type_errors.TypeError (ctx,te) ->
raise (NotDefinable (BadTypedProj (fid,ctx,te)))
in
- let refi = ConstRef kn in
+ let refi = GlobRef.ConstRef kn in
Impargs.maybe_declare_manual_implicits false refi impls;
if flags.pf_subclass then begin
- let cl = Class.class_of_global (IndRef indsp) in
+ let cl = Class.class_of_global (GlobRef.IndRef indsp) in
Class.try_add_new_coercion_with_source refi ~local:false ~poly ~source:cl
end;
let i = if is_local_assum decl then i+1 else i in
@@ -468,7 +467,7 @@ let declare_structure ~cumulative finite ubinders univs paramimpls params templa
let rsp = (kn, i) in (* This is ind path of idstruc *)
let cstr = (rsp, 1) in
let kinds,sp_projs = declare_projections rsp ctx ~kind binder_name.(i) coers fieldimpls fields in
- let build = ConstructRef cstr in
+ let build = GlobRef.ConstructRef cstr in
let () = if is_coe then Class.try_add_new_coercion build ~local:false ~poly in
let () = declare_structure_entry (cstr, List.rev kinds, List.rev sp_projs) in
rsp
@@ -514,9 +513,9 @@ let declare_class def cumulative ubinders univs id idbuild paramimpls params ari
let proj_cst = Declare.declare_constant ~name:proj_name
(DefinitionEntry proj_entry) ~kind:Decls.(IsDefinition Definition)
in
- let cref = ConstRef cst in
+ let cref = GlobRef.ConstRef cst in
Impargs.declare_manual_implicits false cref paramimpls;
- Impargs.declare_manual_implicits false (ConstRef proj_cst) (List.hd fieldimpls);
+ Impargs.declare_manual_implicits false (GlobRef.ConstRef proj_cst) (List.hd fieldimpls);
Classes.set_typeclass_transparency (EvalConstRef cst) false false;
let sub = match List.hd coers with
| Some b -> Some ((if b then Backward else Forward), List.hd priorities)
@@ -537,7 +536,7 @@ let declare_class def cumulative ubinders univs id idbuild paramimpls params ari
let map ind =
let l = List.map3 (fun decl b y -> RelDecl.get_name decl, b, y)
(List.rev fields) coers (Recordops.lookup_projections ind)
- in IndRef ind, l
+ in GlobRef.IndRef ind, l
in
List.map map inds
in
@@ -580,14 +579,14 @@ let declare_class def cumulative ubinders univs id idbuild paramimpls params ari
let add_constant_class env sigma cst =
- let ty, univs = Typeops.type_of_global_in_context env (ConstRef cst) in
+ let ty, univs = Typeops.type_of_global_in_context env (GlobRef.ConstRef cst) in
let r = (Environ.lookup_constant cst env).const_relevance in
let ctx, _ = decompose_prod_assum ty in
let args = Context.Rel.to_extended_vect Constr.mkRel 0 ctx in
let t = mkApp (mkConstU (cst, Univ.make_abstract_instance univs), args) in
let tc =
{ cl_univs = univs;
- cl_impl = ConstRef cst;
+ cl_impl = GlobRef.ConstRef cst;
cl_context = (List.map (const None) ctx, ctx);
cl_props = [LocalAssum (make_annot Anonymous r, t)];
cl_projs = [];
@@ -609,7 +608,7 @@ let add_inductive_class env sigma ind =
let ty = Inductive.type_of_inductive env ((mind, oneind), inst) in
let r = Inductive.relevance_of_inductive env ind in
{ cl_univs = univs;
- cl_impl = IndRef ind;
+ cl_impl = GlobRef.IndRef ind;
cl_context = List.map (const None) ctx, ctx;
cl_props = [LocalAssum (make_annot Anonymous r, ty)];
cl_projs = [];
@@ -628,8 +627,8 @@ let declare_existing_class g =
if Typeclasses.is_class g then warn_already_existing_class g
else
match g with
- | ConstRef x -> add_constant_class env sigma x
- | IndRef x -> add_inductive_class env sigma x
+ | GlobRef.ConstRef x -> add_constant_class env sigma x
+ | GlobRef.IndRef x -> add_inductive_class env sigma x
| _ -> user_err ~hdr:"declare_existing_class"
(Pp.str"Unsupported class type, only constants and inductives are allowed")
@@ -710,4 +709,4 @@ let definition_structure udecl kind ~template ~cumulative ~poly finite records =
in
let data = List.map2 map data records in
let inds = declare_structure ~cumulative finite ubinders univs implpars params template data in
- List.map (fun ind -> IndRef ind) inds
+ List.map (fun ind -> GlobRef.IndRef ind) inds
diff --git a/vernac/search.ml b/vernac/search.ml
index 964d01260b..06554aae20 100644
--- a/vernac/search.ml
+++ b/vernac/search.ml
@@ -17,7 +17,6 @@ open Libobject
open Environ
open Pattern
open Libnames
-open Globnames
module NamedDecl = Context.Named.Declaration
@@ -53,7 +52,7 @@ module SearchBlacklist =
let iter_constructors indsp u fn env nconstr =
for i = 1 to nconstr do
let typ = Inductiveops.type_of_constructor env ((indsp, i), u) in
- fn (ConstructRef (indsp, i)) env typ
+ fn (GlobRef.ConstructRef (indsp, i)) env typ
done
let iter_named_context_name_type f =
@@ -67,7 +66,7 @@ let get_current_or_goal_context ?pstate glnum =
(* General search over hypothesis of a goal *)
let iter_hypothesis ?pstate glnum (fn : GlobRef.t -> env -> constr -> unit) =
let env = Global.env () in
- let iter_hyp idh typ = fn (VarRef idh) env typ in
+ let iter_hyp idh typ = fn (GlobRef.VarRef idh) env typ in
let evmap,e = get_current_or_goal_context ?pstate glnum in
let pfctxt = named_context e in
iter_named_context_name_type iter_hyp pfctxt
@@ -75,14 +74,14 @@ let iter_hypothesis ?pstate glnum (fn : GlobRef.t -> env -> constr -> unit) =
(* General search over declarations *)
let iter_declarations (fn : GlobRef.t -> env -> constr -> unit) =
let env = Global.env () in
- List.iter (fun d -> fn (VarRef (NamedDecl.get_id d)) env (NamedDecl.get_type d))
+ List.iter (fun d -> fn (GlobRef.VarRef (NamedDecl.get_id d)) env (NamedDecl.get_type d))
(Environ.named_context env);
let iter_obj (sp, kn) lobj = match lobj with
| AtomicObject o ->
begin match object_tag o with
| "CONSTANT" ->
let cst = Global.constant_of_delta_kn kn in
- let gr = ConstRef cst in
+ let gr = GlobRef.ConstRef cst in
let (typ, _) = Typeops.type_of_global_in_context (Global.env ()) gr in
fn gr env typ
| "INDUCTIVE" ->
@@ -93,7 +92,7 @@ let iter_declarations (fn : GlobRef.t -> env -> constr -> unit) =
let u = Univ.make_abstract_instance (Declareops.inductive_polymorphic_context mib) in
let i = (ind, u) in
let typ = Inductiveops.type_of_inductive env i in
- let () = fn (IndRef ind) env typ in
+ let () = fn (GlobRef.IndRef ind) env typ in
let len = Array.length mip.mind_user_lc in
iter_constructors ind u fn env len
in
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 255283ba36..68b7462bde 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -286,8 +286,8 @@ let print_strategy r =
match r with
| None ->
let fold key lvl (vacc, cacc) = match key with
- | VarKey id -> ((VarRef id, lvl) :: vacc, cacc)
- | ConstKey cst -> (vacc, (ConstRef cst, lvl) :: cacc)
+ | VarKey id -> ((GlobRef.VarRef id, lvl) :: vacc, cacc)
+ | ConstKey cst -> (vacc, (GlobRef.ConstRef cst, lvl) :: cacc)
| RelKey _ -> (vacc, cacc)
in
let var_lvl, cst_lvl = fold_strategy fold oracle ([], []) in
@@ -304,7 +304,7 @@ let print_strategy r =
var_msg ++ cst_msg
| Some r ->
let r = Smartlocate.smart_global r in
- let key = match r with
+ let key = let open GlobRef in match r with
| VarRef id -> VarKey id
| ConstRef cst -> ConstKey cst
| IndRef _ | ConstructRef _ -> user_err Pp.(str "The reference is not unfoldable")
@@ -1459,7 +1459,7 @@ let vernac_arguments ~section_local reference args more_implicits nargs_for_red
if red_modifiers_specified then begin
match sr with
- | ConstRef _ as c ->
+ | GlobRef.ConstRef _ as c ->
Reductionops.ReductionBehaviour.set
~local:section_local c (Option.get red_behavior)
@@ -1731,8 +1731,8 @@ let vernac_set_strategy ~local l =
let local = Option.default false local in
let glob_ref r =
match smart_global r with
- | ConstRef sp -> EvalConstRef sp
- | VarRef id -> EvalVarRef id
+ | GlobRef.ConstRef sp -> EvalConstRef sp
+ | GlobRef.VarRef id -> EvalVarRef id
| _ -> user_err Pp.(str
"cannot set an inductive type or a constructor as transparent") in
let l = List.map (fun (lev,ql) -> (lev,List.map glob_ref ql)) l in
@@ -1742,8 +1742,8 @@ let vernac_set_opacity ~local (v,l) =
let local = Option.default true local in
let glob_ref r =
match smart_global r with
- | ConstRef sp -> EvalConstRef sp
- | VarRef id -> EvalVarRef id
+ | GlobRef.ConstRef sp -> EvalConstRef sp
+ | GlobRef.VarRef id -> EvalVarRef id
| _ -> user_err Pp.(str
"cannot set an inductive type or a constructor as transparent") in
let l = List.map glob_ref l in
@@ -2090,7 +2090,7 @@ let vernac_register qid r =
match r with
| RegisterInline ->
begin match gr with
- | ConstRef c -> Global.register_inline c
+ | GlobRef.ConstRef c -> Global.register_inline c
| _ -> CErrors.user_err (Pp.str "Register Inline: expecting a constant")
end
| RegisterCoqlib n ->
@@ -2106,7 +2106,7 @@ let vernac_register qid r =
| k -> CErrors.user_err Pp.(str "Register: unknown identifier “" ++ str k ++ str "” in the “kernel” namespace")
in
match gr with
- | IndRef ind -> Global.register_inductive ind pind
+ | GlobRef.IndRef ind -> Global.register_inductive ind pind
| _ -> CErrors.user_err (Pp.str "Register in kernel: expecting an inductive type")
end
else Coqlib.register_ref (Libnames.string_of_qualid n) gr
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-03 12:45:24 +0000