aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac
diff options
context:
space:
mode:
Diffstat (limited to 'vernac')
-rw-r--r--vernac/assumptions.ml12
-rw-r--r--vernac/assumptions.mli2
-rw-r--r--vernac/auto_ind_decl.ml14
-rw-r--r--vernac/class.ml4
-rw-r--r--vernac/classes.ml2
-rw-r--r--vernac/command.mli2
-rw-r--r--vernac/himsg.ml16
-rw-r--r--vernac/indschemes.ml2
-rw-r--r--vernac/indschemes.mli8
-rw-r--r--vernac/lemmas.ml2
-rw-r--r--vernac/record.mli2
-rw-r--r--vernac/vernacentries.ml6
12 files changed, 36 insertions, 36 deletions
diff --git a/vernac/assumptions.ml b/vernac/assumptions.ml
index 6711b14da..09e645eea 100644
--- a/vernac/assumptions.ml
+++ b/vernac/assumptions.ml
@@ -89,7 +89,7 @@ and fields_of_mp mp =
let mb = lookup_module_in_impl mp in
let fields,inner_mp,subs = fields_of_mb empty_subst mb [] in
let subs =
- if mp_eq inner_mp mp then subs
+ if ModPath.equal inner_mp mp then subs
else add_mp inner_mp mp mb.mod_delta subs
in
Modops.subst_structure subs fields
@@ -118,7 +118,7 @@ and fields_of_expression x = fields_of_functor fields_of_expr x
let lookup_constant_in_impl cst fallback =
try
- let mp,dp,lab = repr_kn (canonical_con cst) in
+ let mp,dp,lab = KerName.repr (Constant.canonical cst) in
let fields = memoize_fields_of_mp mp in
(* A module found this way is necessarily closed, in particular
our constant cannot be in an opened section : *)
@@ -131,7 +131,7 @@ let lookup_constant_in_impl cst fallback =
- The label has not been found in the structure. This is an error *)
match fallback with
| Some cb -> cb
- | None -> anomaly (str "Print Assumption: unknown constant " ++ pr_con cst ++ str ".")
+ | None -> anomaly (str "Print Assumption: unknown constant " ++ Constant.print cst ++ str ".")
let lookup_constant cst =
try
@@ -142,7 +142,7 @@ let lookup_constant cst =
let lookup_mind_in_impl mind =
try
- let mp,dp,lab = repr_kn (canonical_mind mind) in
+ let mp,dp,lab = KerName.repr (MutInd.canonical mind) in
let fields = memoize_fields_of_mp mp in
search_mind_label lab fields
with Not_found ->
@@ -156,9 +156,9 @@ let lookup_mind mind =
traversed objects *)
let label_of = function
- | ConstRef kn -> pi3 (repr_con kn)
+ | ConstRef kn -> pi3 (Constant.repr3 kn)
| IndRef (kn,_)
- | ConstructRef ((kn,_),_) -> pi3 (repr_mind kn)
+ | ConstructRef ((kn,_),_) -> pi3 (MutInd.repr3 kn)
| VarRef id -> Label.of_id id
let fold_constr_with_full_binders g f n acc c =
diff --git a/vernac/assumptions.mli b/vernac/assumptions.mli
index 46730f824..77eb968d4 100644
--- a/vernac/assumptions.mli
+++ b/vernac/assumptions.mli
@@ -21,7 +21,7 @@ open Printer
val traverse :
Label.t -> constr ->
(Refset_env.t * Refset_env.t Refmap_env.t *
- (label * Context.Rel.t * types) list Refmap_env.t)
+ (Label.t * Context.Rel.t * types) list Refmap_env.t)
(** Collects all the assumptions (optionally including opaque definitions)
on which a term relies (together with their type). The above warning of
diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml
index 66a4a2e49..539e5550f 100644
--- a/vernac/auto_ind_decl.ml
+++ b/vernac/auto_ind_decl.ml
@@ -199,7 +199,7 @@ let build_beq_scheme mode kn =
| Cast (x,_,_) -> aux (EConstr.applist (x,a))
| App _ -> assert false
| Ind ((kn',i as ind'),u) (*FIXME: universes *) ->
- if eq_mind kn kn' then mkRel(eqA-nlist-i+nb_ind-1), Safe_typing.empty_private_constants
+ if MutInd.equal kn kn' then mkRel(eqA-nlist-i+nb_ind-1), Safe_typing.empty_private_constants
else begin
try
let eq, eff =
@@ -367,8 +367,8 @@ let do_replace_lb mode lb_scheme_key aavoid narg p q =
(* if this happen then the args have to be already declared as a
Parameter*)
(
- let mp,dir,lbl = repr_con (fst (destConst sigma v)) in
- mkConst (make_con mp dir (mk_label (
+ let mp,dir,lbl = Constant.repr3 (fst (destConst sigma v)) in
+ mkConst (Constant.make3 mp dir (Label.make (
if Int.equal offset 1 then ("eq_"^(Label.to_string lbl))
else ((Label.to_string lbl)^"_lb")
)))
@@ -428,8 +428,8 @@ let do_replace_bl mode bl_scheme_key (ind,u as indu) aavoid narg lft rgt =
(* if this happen then the args have to be already declared as a
Parameter*)
(
- let mp,dir,lbl = repr_con (fst (destConst sigma v)) in
- mkConst (make_con mp dir (mk_label (
+ let mp,dir,lbl = Constant.repr3 (fst (destConst sigma v)) in
+ mkConst (Constant.make3 mp dir (Label.make (
if Int.equal offset 1 then ("eq_"^(Label.to_string lbl))
else ((Label.to_string lbl)^"_bl")
)))
@@ -504,7 +504,7 @@ let do_replace_bl mode bl_scheme_key (ind,u as indu) aavoid narg lft rgt =
with DestKO -> Tacticals.New.tclZEROMSG (str "The expected type is an inductive one.")
end
end >>= fun (sp2,i2) ->
- if not (eq_mind sp1 sp2) || not (Int.equal i1 i2)
+ if not (MutInd.equal sp1 sp2) || not (Int.equal i1 i2)
then Tacticals.New.tclZEROMSG (str "Eq should be on the same type")
else aux (Array.to_list ca1) (Array.to_list ca2)
@@ -531,7 +531,7 @@ let eqI ind l =
and e, eff =
try let c, eff = find_scheme beq_scheme_kind ind in mkConst c, eff
with Not_found -> user_err ~hdr:"AutoIndDecl.eqI"
- (str "The boolean equality on " ++ pr_mind (fst ind) ++ str " is needed.");
+ (str "The boolean equality on " ++ MutInd.print (fst ind) ++ str " is needed.");
in (if Array.equal Term.eq_constr eA [||] then e else mkApp(e,eA)), eff
(**********************************************************************)
diff --git a/vernac/class.ml b/vernac/class.ml
index 3915148a0..061f3efcc 100644
--- a/vernac/class.ml
+++ b/vernac/class.ml
@@ -173,8 +173,8 @@ let get_strength stre ref cls clt =
let ident_key_of_class = function
| CL_FUN -> "Funclass"
| CL_SORT -> "Sortclass"
- | CL_CONST sp | CL_PROJ sp -> Label.to_string (con_label sp)
- | CL_IND (sp,_) -> Label.to_string (mind_label sp)
+ | CL_CONST sp | CL_PROJ sp -> Label.to_string (Constant.label sp)
+ | CL_IND (sp,_) -> Label.to_string (MutInd.label sp)
| CL_SECVAR id -> Id.to_string id
(* Identity coercion *)
diff --git a/vernac/classes.ml b/vernac/classes.ml
index 0926c93e5..9a8fc9bc2 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -98,7 +98,7 @@ let type_ctx_instance evars env ctx inst subst =
let id_of_class cl =
match cl.cl_impl with
- | ConstRef kn -> let _,_,l = repr_con kn in Label.to_id l
+ | ConstRef kn -> let _,_,l = Constant.repr3 kn in Label.to_id l
| IndRef (kn,i) ->
let mip = (Environ.lookup_mind kn (Global.env ())).Declarations.mind_packets in
mip.(0).Declarations.mind_typename
diff --git a/vernac/command.mli b/vernac/command.mli
index afa97aa24..26b1d1aaf 100644
--- a/vernac/command.mli
+++ b/vernac/command.mli
@@ -90,7 +90,7 @@ val interp_mutual_inductive :
val declare_mutual_inductive_with_eliminations :
mutual_inductive_entry -> Universes.universe_binders -> one_inductive_impls list ->
- mutual_inductive
+ MutInd.t
(** Entry points for the vernacular commands Inductive and CoInductive *)
diff --git a/vernac/himsg.ml b/vernac/himsg.ml
index 189c47aab..7b1a948ed 100644
--- a/vernac/himsg.ml
+++ b/vernac/himsg.ml
@@ -899,11 +899,11 @@ let explain_not_match_error = function
quote (Univ.pr_constraints (Termops.pr_evd_level Evd.empty) cst)
let explain_signature_mismatch l spec why =
- str "Signature components for label " ++ pr_label l ++
+ str "Signature components for label " ++ Label.print l ++
str " do not match:" ++ spc () ++ explain_not_match_error why ++ str "."
let explain_label_already_declared l =
- str "The label " ++ pr_label l ++ str " is already declared."
+ str "The label " ++ Label.print l ++ str " is already declared."
let explain_application_to_not_path _ =
strbrk "A module cannot be applied to another module application or " ++
@@ -933,11 +933,11 @@ let explain_not_equal_module_paths mp1 mp2 =
str "Non equal modules."
let explain_no_such_label l =
- str "No such label " ++ pr_label l ++ str "."
+ str "No such label " ++ Label.print l ++ str "."
let explain_incompatible_labels l l' =
str "Opening and closing labels are not the same: " ++
- pr_label l ++ str " <> " ++ pr_label l' ++ str "!"
+ Label.print l ++ str " <> " ++ Label.print l' ++ str "!"
let explain_not_a_module s =
quote (str s) ++ str " is not a module."
@@ -946,19 +946,19 @@ let explain_not_a_module_type s =
quote (str s) ++ str " is not a module type."
let explain_not_a_constant l =
- quote (pr_label l) ++ str " is not a constant."
+ quote (Label.print l) ++ str " is not a constant."
let explain_incorrect_label_constraint l =
str "Incorrect constraint for label " ++
- quote (pr_label l) ++ str "."
+ quote (Label.print l) ++ str "."
let explain_generative_module_expected l =
- str "The module " ++ pr_label l ++ str " is not generative." ++
+ str "The module " ++ Label.print l ++ str " is not generative." ++
strbrk " Only components of generative modules can be changed" ++
strbrk " using the \"with\" construct."
let explain_label_missing l s =
- str "The field " ++ pr_label l ++ str " is missing in "
+ str "The field " ++ Label.print l ++ str " is missing in "
++ str s ++ str "."
let explain_include_restricted_functor mp =
diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml
index 90168843a..4bdc93a36 100644
--- a/vernac/indschemes.ml
+++ b/vernac/indschemes.ml
@@ -407,7 +407,7 @@ let do_mutual_induction_scheme lnamedepindsort =
let get_common_underlying_mutual_inductive = function
| [] -> assert false
| (id,(mind,i as ind))::l as all ->
- match List.filter (fun (_,(mind',_)) -> not (eq_mind mind mind')) l with
+ match List.filter (fun (_,(mind',_)) -> not (MutInd.equal mind mind')) l with
| (_,ind')::_ ->
raise (RecursionSchemeError (NotMutualInScheme (ind,ind')))
| [] ->
diff --git a/vernac/indschemes.mli b/vernac/indschemes.mli
index 91c4c5825..659f12936 100644
--- a/vernac/indschemes.mli
+++ b/vernac/indschemes.mli
@@ -16,9 +16,9 @@ open Vernacexpr
(** Build and register the boolean equalities associated to an inductive type *)
-val declare_beq_scheme : mutual_inductive -> unit
+val declare_beq_scheme : MutInd.t -> unit
-val declare_eq_decidability : mutual_inductive -> unit
+val declare_eq_decidability : MutInd.t -> unit
(** Build and register a congruence scheme for an equality-like inductive type *)
@@ -39,10 +39,10 @@ val do_scheme : (Id.t located option * scheme) list -> unit
(** Combine a list of schemes into a conjunction of them *)
-val build_combined_scheme : env -> constant list -> Evd.evar_map * constr * types
+val build_combined_scheme : env -> Constant.t list -> Evd.evar_map * constr * types
val do_combined_scheme : Id.t located -> Id.t located list -> unit
(** Hook called at each inductive type definition *)
-val declare_default_schemes : mutual_inductive -> unit
+val declare_default_schemes : MutInd.t -> unit
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index dbf7fec66..22f0d199c 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -116,7 +116,7 @@ let find_mutually_recursive_statements thms =
[] in
ind_hyps,ind_ccl) thms in
let inds_hyps,ind_ccls = List.split inds in
- let of_same_mutind ((kn,_),_,_) = function ((kn',_),_,_) -> eq_mind kn kn' in
+ let of_same_mutind ((kn,_),_,_) = function ((kn',_),_,_) -> MutInd.equal kn kn' in
(* Check if all conclusions are coinductive in the same type *)
(* (degenerated cartesian product since there is at most one coind ccl) *)
let same_indccl =
diff --git a/vernac/record.mli b/vernac/record.mli
index aea474581..1bcbf39b7 100644
--- a/vernac/record.mli
+++ b/vernac/record.mli
@@ -22,7 +22,7 @@ val primitive_flag : bool ref
val declare_projections :
inductive -> ?kind:Decl_kinds.definition_object_kind -> Id.t ->
coercion_flag list -> manual_explicitation list list -> Context.Rel.t ->
- (Name.t * bool) list * constant option list
+ (Name.t * bool) list * Constant.t option list
val declare_structure :
Decl_kinds.recursivity_kind ->
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 41f63644d..7eedf24f8 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -250,7 +250,7 @@ let print_namespace ns =
let print_list pr l = prlist_with_sep (fun () -> str".") pr l in
let print_kn kn =
(* spiwack: I'm ignoring the dirpath, is that bad? *)
- let (mp,_,lbl) = Names.repr_kn kn in
+ let (mp,_,lbl) = Names.KerName.repr kn in
let qn = (qualified_minus (List.length ns) mp)@[Names.Label.to_id lbl] in
print_list pr_id qn
in
@@ -265,8 +265,8 @@ let print_namespace ns =
let constants = (Environ.pre_env (Global.env ())).Pre_env.env_globals.Pre_env.env_constants in
let constants_in_namespace =
Cmap_env.fold (fun c (body,_) acc ->
- let kn = user_con c in
- if matches (modpath kn) then
+ let kn = Constant.user c in
+ if matches (KerName.modpath kn) then
acc++fnl()++hov 2 (print_constant kn body)
else
acc
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-13 09:08:57 +0000