aboutsummaryrefslogtreecommitdiff
path: root/plugins
diff options
context:
space:
mode:
Diffstat (limited to 'plugins')
-rw-r--r--plugins/extraction/common.ml2
-rw-r--r--plugins/extraction/extract_env.ml8
-rw-r--r--plugins/extraction/table.ml17
-rw-r--r--plugins/extraction/table.mli2
-rw-r--r--plugins/funind/functional_principles_types.ml12
-rw-r--r--plugins/funind/indfun.ml4
-rw-r--r--plugins/funind/indfun_common.ml31
-rw-r--r--plugins/funind/invfun.ml2
-rw-r--r--plugins/omega/g_omega.mlg2
-rw-r--r--plugins/setoid_ring/newring.ml4
-rw-r--r--plugins/ssr/ssrequality.ml4
-rw-r--r--plugins/syntax/ascii_syntax.ml5
-rw-r--r--plugins/syntax/r_syntax.ml14
-rw-r--r--plugins/syntax/string_syntax.ml3
14 files changed, 39 insertions, 71 deletions
diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml
index d413cd1e6d..bdeb6fca60 100644
--- a/plugins/extraction/common.ml
+++ b/plugins/extraction/common.ml
@@ -588,7 +588,7 @@ let pp_global k r =
let ls = ref_renaming (k,r) in
assert (List.length ls > 1);
let s = List.hd ls in
- let mp,_,l = repr_of_r r in
+ let mp,l = repr_of_r r in
if ModPath.equal mp (top_visible_mp ()) then
(* simpliest situation: definition of r (or use in the same context) *)
(* we update the visible environment *)
diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml
index 5d3115d8d7..b0f6301192 100644
--- a/plugins/extraction/extract_env.ml
+++ b/plugins/extraction/extract_env.ml
@@ -30,7 +30,7 @@ open Common
let toplevel_env () =
let get_reference = function
| (_,kn), Lib.Leaf o ->
- let mp,_,l = KerName.repr kn in
+ let mp,l = KerName.repr kn in
begin match Libobject.object_tag o with
| "CONSTANT" ->
let constant = Global.lookup_constant (Constant.make1 kn) in
@@ -124,7 +124,7 @@ module Visit : VISIT = struct
end
let add_field_label mp = function
- | (lab, (SFBconst _|SFBmind _)) -> Visit.add_kn (KerName.make2 mp lab)
+ | (lab, (SFBconst _|SFBmind _)) -> Visit.add_kn (KerName.make mp lab)
| (lab, (SFBmodule _|SFBmodtype _)) -> Visit.add_mp_all (MPdot (mp,lab))
let rec add_labels mp = function
@@ -208,10 +208,10 @@ let env_for_mtb_with_def env mp me reso idl =
Modops.add_structure mp before reso env
let make_cst resolver mp l =
- Mod_subst.constant_of_delta_kn resolver (KerName.make2 mp l)
+ Mod_subst.constant_of_delta_kn resolver (KerName.make mp l)
let make_mind resolver mp l =
- Mod_subst.mind_of_delta_kn resolver (KerName.make2 mp l)
+ Mod_subst.mind_of_delta_kn resolver (KerName.make mp l)
(* From a [structure_body] (i.e. a list of [structure_field_body])
to specifications. *)
diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml
index 6ee1770a4e..7b4fd280bd 100644
--- a/plugins/extraction/table.ml
+++ b/plugins/extraction/table.ml
@@ -36,16 +36,16 @@ let occur_kn_in_ref kn = function
| ConstRef _ | VarRef _ -> false
let repr_of_r = function
- | ConstRef kn -> Constant.repr3 kn
+ | ConstRef kn -> Constant.repr2 kn
| IndRef (kn,_)
- | ConstructRef ((kn,_),_) -> MutInd.repr3 kn
+ | ConstructRef ((kn,_),_) -> MutInd.repr2 kn
| VarRef v -> KerName.repr (Lib.make_kn v)
let modpath_of_r r =
- let mp,_,_ = repr_of_r r in mp
+ let mp,_ = repr_of_r r in mp
let label_of_r r =
- let _,_,l = repr_of_r r in l
+ let _,l = repr_of_r r in l
let rec base_mp = function
| MPdot (mp,l) -> base_mp mp
@@ -95,7 +95,7 @@ let rec parse_labels2 ll mp1 = function
let labels_of_ref r =
let mp_top = Lib.current_mp () in
- let mp,_,l = repr_of_r r in
+ let mp,l = repr_of_r r in
parse_labels2 [l] mp_top mp
@@ -189,7 +189,7 @@ let init_recursors () = recursors := KNset.empty
let add_recursors env ind =
let kn = MutInd.canonical ind in
let mk_kn id =
- KerName.make (KerName.modpath kn) DirPath.empty (Label.of_id id)
+ KerName.make (KerName.modpath kn) (Label.of_id id)
in
let mib = Environ.lookup_mind ind env in
Array.iter
@@ -287,7 +287,7 @@ let safe_pr_long_global r =
try Printer.pr_global r
with Not_found -> match r with
| ConstRef kn ->
- let mp,_,l = Constant.repr3 kn in
+ let mp,l = Constant.repr2 kn in
str ((ModPath.to_string mp)^"."^(Label.to_string l))
| _ -> assert false
@@ -653,8 +653,7 @@ let inline_extraction : bool * GlobRef.t list -> obj =
cache_function = (fun (_,(b,l)) -> add_inline_entries b l);
load_function = (fun _ (_,(b,l)) -> add_inline_entries b l);
classify_function = (fun o -> Substitute o);
- discharge_function =
- (fun (_,(b,l)) -> Some (b, List.map pop_global_reference l));
+ discharge_function = (fun (_,x) -> Some x);
subst_function =
(fun (s,(b,l)) -> (b,(List.map (fun x -> fst (subst_global s x)) l)))
}
diff --git a/plugins/extraction/table.mli b/plugins/extraction/table.mli
index a8baeaf1b6..acc1bfee8a 100644
--- a/plugins/extraction/table.mli
+++ b/plugins/extraction/table.mli
@@ -46,7 +46,7 @@ val info_file : string -> unit
(*s utilities about [module_path] and [kernel_names] and [GlobRef.t] *)
val occur_kn_in_ref : MutInd.t -> GlobRef.t -> bool
-val repr_of_r : GlobRef.t -> ModPath.t * DirPath.t * Label.t
+val repr_of_r : GlobRef.t -> ModPath.t * Label.t
val modpath_of_r : GlobRef.t -> ModPath.t
val label_of_r : GlobRef.t -> Label.t
val base_mp : ModPath.t -> ModPath.t
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index b2a528a1fd..839915631d 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -394,7 +394,7 @@ let generate_functional_principle (evd: Evd.evar_map ref)
exception Not_Rec
-let get_funs_constant mp dp =
+let get_funs_constant mp =
let get_funs_constant const e : (Names.Constant.t*int) array =
match Constr.kind ((strip_lam e)) with
| Fix((_,(na,_,_))) ->
@@ -402,7 +402,7 @@ let get_funs_constant mp dp =
(fun i na ->
match na with
| Name id ->
- let const = Constant.make3 mp dp (Label.of_id id) in
+ let const = Constant.make2 mp (Label.of_id id) in
const,i
| Anonymous ->
anomaly (Pp.str "Anonymous fix.")
@@ -474,13 +474,13 @@ let make_scheme evd (fas : (pconstant*Sorts.family) list) : Safe_typing.private_
let env = Global.env () in
let funs = List.map fst fas in
let first_fun = List.hd funs in
- let funs_mp,funs_dp,_ = KerName.repr (Constant.canonical (fst first_fun)) in
+ let funs_mp = KerName.modpath (Constant.canonical (fst first_fun)) in
let first_fun_kn =
try
fst (find_Function_infos (fst first_fun)).graph_ind
with Not_found -> raise No_graph_found
in
- let this_block_funs_indexes = get_funs_constant funs_mp funs_dp (fst first_fun) in
+ let this_block_funs_indexes = get_funs_constant funs_mp (fst first_fun) in
let this_block_funs = Array.map (fun (c,_) -> (c,snd first_fun)) this_block_funs_indexes in
let prop_sort = InProp in
let funs_indexes =
@@ -669,9 +669,9 @@ let build_case_scheme fa =
user_err ~hdr:"FunInd.build_case_scheme"
(str "Cannot find " ++ Libnames.pr_qualid f) in
let first_fun,u = destConst funs in
- let funs_mp,funs_dp,_ = Constant.repr3 first_fun in
+ let funs_mp = Constant.modpath first_fun in
let first_fun_kn = try fst (find_Function_infos first_fun).graph_ind with Not_found -> raise No_graph_found in
- let this_block_funs_indexes = get_funs_constant funs_mp funs_dp first_fun in
+ let this_block_funs_indexes = get_funs_constant funs_mp first_fun in
let this_block_funs = Array.map (fun (c,_) -> (c,u)) this_block_funs_indexes in
let prop_sort = InProp in
let funs_indexes =
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 9eda19a86b..9a6169d42a 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -898,11 +898,11 @@ let make_graph (f_ref : GlobRef.t) =
let id = Label.to_id (Constant.label c) in
[((CAst.make id,None),(None,Constrexpr.CStructRec),nal_tas,t,Some b),[]]
in
- let mp,dp,_ = Constant.repr3 c in
+ let mp = Constant.modpath c in
do_generate_principle [c,Univ.Instance.empty] error_error false false expr_list;
(* We register the infos *)
List.iter
- (fun ((({CAst.v=id},_),_,_,_,_),_) -> add_Function false (Constant.make3 mp dp (Label.of_id id)))
+ (fun ((({CAst.v=id},_),_,_,_,_),_) -> add_Function false (Constant.make2 mp (Label.of_id id)))
expr_list)
let do_generate_principle = do_generate_principle [] warning_error true
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index 4eee2c7a45..6ed382ca1c 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -297,36 +297,7 @@ let subst_Function (subst,finfos) =
let classify_Function infos = Libobject.Substitute infos
-let discharge_Function (_,finfos) =
- let function_constant' = Lib.discharge_con finfos.function_constant
- and graph_ind' = Lib.discharge_inductive finfos.graph_ind
- and equation_lemma' = Option.Smart.map Lib.discharge_con finfos.equation_lemma
- and correctness_lemma' = Option.Smart.map Lib.discharge_con finfos.correctness_lemma
- and completeness_lemma' = Option.Smart.map Lib.discharge_con finfos.completeness_lemma
- and rect_lemma' = Option.Smart.map Lib.discharge_con finfos.rect_lemma
- and rec_lemma' = Option.Smart.map Lib.discharge_con finfos.rec_lemma
- and prop_lemma' = Option.Smart.map Lib.discharge_con finfos.prop_lemma
- in
- if function_constant' == finfos.function_constant &&
- graph_ind' == finfos.graph_ind &&
- equation_lemma' == finfos.equation_lemma &&
- correctness_lemma' == finfos.correctness_lemma &&
- completeness_lemma' == finfos.completeness_lemma &&
- rect_lemma' == finfos.rect_lemma &&
- rec_lemma' == finfos.rec_lemma &&
- prop_lemma' == finfos.prop_lemma
- then Some finfos
- else
- Some { function_constant = function_constant' ;
- graph_ind = graph_ind' ;
- equation_lemma = equation_lemma' ;
- correctness_lemma = correctness_lemma' ;
- completeness_lemma = completeness_lemma';
- rect_lemma = rect_lemma';
- rec_lemma = rec_lemma';
- prop_lemma = prop_lemma' ;
- is_general = finfos.is_general
- }
+let discharge_Function (_,finfos) = Some finfos
let pr_ocst c =
let sigma, env = Pfedit.get_current_context () in
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index ad11f853ca..56fe430077 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -450,7 +450,7 @@ let generalize_dependent_of x hyp g =
let tauto =
let dp = List.map Id.of_string ["Tauto" ; "Init"; "Coq"] in
let mp = ModPath.MPfile (DirPath.make dp) in
- let kn = KerName.make2 mp (Label.make "tauto") in
+ let kn = KerName.make mp (Label.make "tauto") in
Proofview.tclBIND (Proofview.tclUNIT ()) begin fun () ->
let body = Tacenv.interp_ltac kn in
Tacinterp.eval_tactic body
diff --git a/plugins/omega/g_omega.mlg b/plugins/omega/g_omega.mlg
index c3d063cff8..85081b24a3 100644
--- a/plugins/omega/g_omega.mlg
+++ b/plugins/omega/g_omega.mlg
@@ -27,7 +27,7 @@ open Stdarg
let eval_tactic name =
let dp = DirPath.make (List.map Id.of_string ["PreOmega"; "omega"; "Coq"]) in
- let kn = KerName.make2 (ModPath.MPfile dp) (Label.make name) in
+ let kn = KerName.make (ModPath.MPfile dp) (Label.make name) in
let tac = Tacenv.interp_ltac kn in
Tacinterp.eval_tactic tac
diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml
index b05e1e85b7..0734654abf 100644
--- a/plugins/setoid_ring/newring.ml
+++ b/plugins/setoid_ring/newring.ml
@@ -266,7 +266,7 @@ let my_reference c =
let znew_ring_path =
DirPath.make (List.map Id.of_string ["InitialRing";plugin_dir;"Coq"])
let zltac s =
- lazy(KerName.make (ModPath.MPfile znew_ring_path) DirPath.empty (Label.make s))
+ lazy(KerName.make (ModPath.MPfile znew_ring_path) (Label.make s))
let mk_cst l s = lazy (Coqlib.coq_reference "newring" l s);;
let pol_cst s = mk_cst [plugin_dir;"Ring_polynom"] s ;;
@@ -760,7 +760,7 @@ let new_field_path =
DirPath.make (List.map Id.of_string ["Field_tac";plugin_dir;"Coq"])
let field_ltac s =
- lazy(KerName.make (ModPath.MPfile new_field_path) DirPath.empty (Label.make s))
+ lazy(KerName.make (ModPath.MPfile new_field_path) (Label.make s))
let _ = add_map "field"
diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml
index f23433f2f4..2af917b939 100644
--- a/plugins/ssr/ssrequality.ml
+++ b/plugins/ssr/ssrequality.ml
@@ -337,9 +337,9 @@ let pirrel_rewrite pred rdx rdx_ty new_rdx dir (sigma, c) c_ty gl =
let elim, gl = pf_fresh_global (Indrec.lookup_eliminator ind sort) gl in
if dir = R2L then elim, gl else (* taken from Coq's rewrite *)
let elim, _ = destConst elim in
- let mp,dp,l = Constant.repr3 (Constant.make1 (Constant.canonical elim)) in
+ let mp,l = Constant.repr2 (Constant.make1 (Constant.canonical elim)) in
let l' = Label.of_id (Nameops.add_suffix (Label.to_id l) "_r") in
- let c1' = Global.constant_of_delta_kn (Constant.canonical (Constant.make3 mp dp l')) in
+ let c1' = Global.constant_of_delta_kn (Constant.canonical (Constant.make2 mp l')) in
mkConst c1', gl in
let elim = EConstr.of_constr elim in
let proof = EConstr.mkApp (elim, [| rdx_ty; new_rdx; pred; p; rdx; c |]) in
diff --git a/plugins/syntax/ascii_syntax.ml b/plugins/syntax/ascii_syntax.ml
index 53153198f9..8ee6fbf036 100644
--- a/plugins/syntax/ascii_syntax.ml
+++ b/plugins/syntax/ascii_syntax.ml
@@ -24,7 +24,6 @@ open Coqlib
exception Non_closed_ascii
let make_dir l = DirPath.make (List.rev_map Id.of_string l)
-let make_kn dir id = Globnames.encode_mind (make_dir dir) (Id.of_string id)
let make_path dir id = Libnames.make_path (make_dir dir) (Id.of_string id)
let is_gr c gr = match DAst.get c with
@@ -32,10 +31,12 @@ let is_gr c gr = match DAst.get c with
| _ -> false
let ascii_module = ["Coq";"Strings";"Ascii"]
+let ascii_modpath = MPfile (make_dir ascii_module)
let ascii_path = make_path ascii_module "ascii"
-let ascii_kn = make_kn ascii_module "ascii"
+let ascii_label = Label.make "ascii"
+let ascii_kn = MutInd.make2 ascii_modpath ascii_label
let path_of_Ascii = ((ascii_kn,0),1)
let static_glob_Ascii = ConstructRef path_of_Ascii
diff --git a/plugins/syntax/r_syntax.ml b/plugins/syntax/r_syntax.ml
index 49497aef54..776d2a2229 100644
--- a/plugins/syntax/r_syntax.ml
+++ b/plugins/syntax/r_syntax.ml
@@ -33,12 +33,10 @@ let is_gr c gr = match DAst.get c with
| GRef (r, _) -> GlobRef.equal r gr
| _ -> false
+let positive_modpath = MPfile (make_dir binnums)
let positive_path = make_path binnums "positive"
-(* TODO: temporary hack *)
-let make_kn dir id = Globnames.encode_mind dir id
-
-let positive_kn = make_kn (make_dir binnums) (Id.of_string "positive")
+let positive_kn = MutInd.make2 positive_modpath (Label.make "positive")
let glob_positive = IndRef (positive_kn,0)
let path_of_xI = ((positive_kn,0),1)
let path_of_xO = ((positive_kn,0),2)
@@ -74,7 +72,7 @@ let rec bignat_of_pos c = match DAst.get c with
(**********************************************************************)
let z_path = make_path binnums "Z"
-let z_kn = make_kn (make_dir binnums) (Id.of_string "Z")
+let z_kn = MutInd.make2 positive_modpath (Label.make "Z")
let glob_z = IndRef (z_kn,0)
let path_of_ZERO = ((z_kn,0),1)
let path_of_POS = ((z_kn,0),2)
@@ -106,12 +104,10 @@ let bigint_of_z c = match DAst.get c with
(**********************************************************************)
let rdefinitions = ["Coq";"Reals";"Rdefinitions"]
+let r_modpath = MPfile (make_dir rdefinitions)
let r_path = make_path rdefinitions "R"
-(* TODO: temporary hack *)
-let make_path dir id = Globnames.encode_con dir (Id.of_string id)
-
-let glob_IZR = ConstRef (make_path (make_dir rdefinitions) "IZR")
+let glob_IZR = ConstRef (Constant.make2 r_modpath @@ Label.make "IZR")
let r_of_int ?loc z =
DAst.make @@ GApp (DAst.make @@ GRef(glob_IZR,None), [z_of_int ?loc z])
diff --git a/plugins/syntax/string_syntax.ml b/plugins/syntax/string_syntax.ml
index 7478c1e978..703b40dd3e 100644
--- a/plugins/syntax/string_syntax.ml
+++ b/plugins/syntax/string_syntax.ml
@@ -24,9 +24,10 @@ exception Non_closed_string
let string_module = ["Coq";"Strings";"String"]
+let string_modpath = MPfile (make_dir string_module)
let string_path = make_path string_module "string"
-let string_kn = make_kn string_module "string"
+let string_kn = MutInd.make2 string_modpath @@ Label.make "string"
let static_glob_EmptyString = ConstructRef ((string_kn,0),1)
let static_glob_String = ConstructRef ((string_kn,0),2)
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 15:32:54 +0000