aboutsummaryrefslogtreecommitdiff
path: root/pretyping
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping')
-rw-r--r--pretyping/cases.ml2
-rw-r--r--pretyping/classops.ml4
-rw-r--r--pretyping/detyping.ml6
-rw-r--r--pretyping/evarconv.ml4
-rw-r--r--pretyping/indrec.ml7
-rw-r--r--pretyping/inductiveops.ml2
-rw-r--r--pretyping/pattern.ml9
-rw-r--r--pretyping/recordops.ml8
-rw-r--r--pretyping/termops.ml21
-rw-r--r--pretyping/typeclasses.ml7
10 files changed, 40 insertions, 30 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 899fb64e1c..9406a57d79 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -488,7 +488,7 @@ let check_and_adjust_constructor env ind cstrs = function
| PatCstr (loc,((_,i) as cstr),args,alias) as pat ->
(* Check it is constructor of the right type *)
let ind' = inductive_of_constructor cstr in
- if Closure.mind_equiv env ind' ind then
+ if eq_ind ind' ind then
(* Check the constructor has the right number of args *)
let ci = cstrs.(i-1) in
let nb_args_constr = ci.cs_nargs in
diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index 35ffda0a1b..7ec77f7dca 100644
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -156,7 +156,7 @@ let subst_cl_typ subst ct = match ct with
if kn' == kn then ct else
fst (find_class_type (Global.env()) Evd.empty t)
| CL_IND (kn,i) ->
- let kn' = subst_kn subst kn in
+ let kn' = subst_ind subst kn in
if kn' == kn then ct else
CL_IND (kn',i)
@@ -355,7 +355,7 @@ let load_coercion i (_,(coe,stre,isid,cls,clt,ps)) =
let cache_coercion o =
load_coercion 1 o
-let subst_coercion (_,subst,(coe,stre,isid,cls,clt,ps as obj)) =
+let subst_coercion (subst,(coe,stre,isid,cls,clt,ps as obj)) =
let coe' = subst_coe_typ subst coe in
let cls' = subst_cl_typ subst cls in
let clt' = subst_cl_typ subst clt in
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index f9c872f9ed..16520916cd 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -70,7 +70,7 @@ module PrintingCasesMake =
type t = inductive * int array
let encode = Test.encode
let subst subst ((kn,i), ints as obj) =
- let kn' = subst_kn subst kn in
+ let kn' = subst_ind subst kn in
if kn' == kn then obj else
(kn',i), ints
let printer (ind,_) = pr_global_env Idset.empty (IndRef ind)
@@ -566,7 +566,7 @@ let rec subst_cases_pattern subst pat =
match pat with
| PatVar _ -> pat
| PatCstr (loc,((kn,i),j),cpl,n) ->
- let kn' = subst_kn subst kn
+ let kn' = subst_ind subst kn
and cpl' = list_smartmap (subst_cases_pattern subst) cpl in
if kn' == kn && cpl' == cpl then pat else
PatCstr (loc,((kn',i),j),cpl',n)
@@ -610,7 +610,7 @@ let rec subst_rawconstr subst raw =
let (n,topt) = x in
let topt' = Option.smartmap
(fun (loc,(sp,i),x,y as t) ->
- let sp' = subst_kn subst sp in
+ let sp' = subst_ind subst sp in
if sp == sp' then t else (loc,(sp',i),x,y)) topt in
if a == a' && topt == topt' then y else (a',(n,topt'))) rl
and branches' = list_smartmap
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index b6e697e4de..10f4db77aa 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -428,12 +428,12 @@ and evar_eqappr_x env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) =
evar_conv_x (push_rel (n,None,c) env) i pbty c'1 c'2)]
| Ind sp1, Ind sp2 ->
- if sp1=sp2 then
+ if eq_ind sp1 sp2 then
ise_list2 evd (fun i -> evar_conv_x env i CONV) l1 l2
else (evd, false)
| Construct sp1, Construct sp2 ->
- if sp1=sp2 then
+ if eq_constructor sp1 sp2 then
ise_list2 evd (fun i -> evar_conv_x env i CONV) l1 l2
else (evd, false)
diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml
index eed795cdcf..f134614cbc 100644
--- a/pretyping/indrec.ml
+++ b/pretyping/indrec.ml
@@ -574,15 +574,16 @@ let make_elimination_ident id s = add_suffix id (elimination_suffix s)
let lookup_eliminator ind_sp s =
let kn,i = ind_sp in
- let mp,dp,l = repr_kn kn in
+ let mp,dp,l = repr_mind kn in
let ind_id = (Global.lookup_mind kn).mind_packets.(i).mind_typename in
let id = add_suffix ind_id (elimination_suffix s) in
(* Try first to get an eliminator defined in the same section as the *)
(* inductive type *)
try
- let cst = make_con mp dp (label_of_id id) in
+ let cst =Global.constant_of_delta
+ (make_con mp dp (label_of_id id)) in
let _ = Global.lookup_constant cst in
- mkConst cst
+ mkConst cst
with Not_found ->
(* Then try to get a user-defined eliminator in some other places *)
(* using short name (e.g. for "eq_rec") *)
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index bfe1522f9c..1f196f43ef 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -471,5 +471,5 @@ let control_only_guard env c =
iter env c
let subst_inductive subst (kn,i as ind) =
- let kn' = Mod_subst.subst_kn subst kn in
+ let kn' = Mod_subst.subst_ind subst kn in
if kn == kn' then ind else (kn',i)
diff --git a/pretyping/pattern.ml b/pretyping/pattern.ml
index be37e6531c..ec4a1260c5 100644
--- a/pretyping/pattern.ml
+++ b/pretyping/pattern.ml
@@ -101,7 +101,7 @@ let rec pattern_of_constr t =
| Prod (na,c,b) -> PProd (na,pattern_of_constr c,pattern_of_constr b)
| Lambda (na,c,b) -> PLambda (na,pattern_of_constr c,pattern_of_constr b)
| App (f,a) -> PApp (pattern_of_constr f,Array.map pattern_of_constr a)
- | Const sp -> PRef (ConstRef sp)
+ | Const sp -> PRef (ConstRef (constant_of_kn(canonical_con sp)))
| Ind sp -> PRef (IndRef sp)
| Construct sp -> PRef (ConstructRef sp)
| Evar (n,ctxt) -> PEvar (n,Array.map pattern_of_constr ctxt)
@@ -212,8 +212,9 @@ let rec pat_of_raw metas vars = function
with Not_found -> PVar id)
| RPatVar (_,(false,n)) ->
metas := n::!metas; PMeta (Some n)
- | RRef (_,r) ->
- PRef r
+ | RRef (_,ConstRef con) ->
+ PRef (ConstRef (constant_of_kn(canonical_con con)))
+ | RRef (_,r) -> PRef r
(* Hack pour ne pas réécrire une interprétation complète des patterns*)
| RApp (_, RPatVar (_,(true,n)), cl) ->
metas := n::!metas; PSoApp (n, List.map (pat_of_raw metas vars) cl)
@@ -295,5 +296,5 @@ and pat_of_raw_branch loc metas vars ind brs i =
let pattern_of_rawconstr c =
let metas = ref [] in
- let p = pat_of_raw metas [] c in
+ let p = pat_of_raw metas [] c in
(!metas,p)
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index 057b263948..13f2aef261 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -52,8 +52,8 @@ let load_structure i (_,(ind,id,kl,projs)) =
let cache_structure o =
load_structure 1 o
-let subst_structure (_,subst,((kn,i),id,kl,projs as obj)) =
- let kn' = subst_kn subst kn in
+let subst_structure (subst,((kn,i),id,kl,projs as obj)) =
+ let kn' = subst_ind subst kn in
let projs' =
(* invariant: struc.s_PROJ is an evaluable reference. Thus we can take *)
(* the first component of subst_con. *)
@@ -136,7 +136,7 @@ let (in_method,out_method) =
{ (default_object "RECMETHODS") with
load_function = (fun _ -> load_method);
cache_function = load_method;
- subst_function = (fun (_,s,(ty,id)) -> Mod_subst.subst_mps s ty,subst_id s id);
+ subst_function = (fun (s,(ty,id)) -> Mod_subst.subst_mps s ty,subst_id s id);
classify_function = (fun x -> Substitute x)
}
@@ -252,7 +252,7 @@ let open_canonical_structure i (_,o) =
let cache_canonical_structure o =
open_canonical_structure 1 o
-let subst_canonical_structure (_,subst,(cst,ind as obj)) =
+let subst_canonical_structure (subst,(cst,ind as obj)) =
(* invariant: cst is an evaluable reference. Thus we can take *)
(* the first component of subst_con. *)
let cst' = fst (subst_con subst cst) in
diff --git a/pretyping/termops.ml b/pretyping/termops.ml
index f0a7ce4c81..3b6d13d471 100644
--- a/pretyping/termops.ml
+++ b/pretyping/termops.ml
@@ -65,9 +65,9 @@ let rec pr_constr c = match kind_of_term c with
(str"Evar#" ++ int e ++ str"{" ++
prlist_with_sep spc pr_constr (Array.to_list l) ++str"}")
| Const c -> str"Cst(" ++ pr_con c ++ str")"
- | Ind (sp,i) -> str"Ind(" ++ pr_path sp ++ str"," ++ int i ++ str")"
+ | Ind (sp,i) -> str"Ind(" ++ pr_mind sp ++ str"," ++ int i ++ str")"
| Construct ((sp,i),j) ->
- str"Constr(" ++ pr_path sp ++ str"," ++ int i ++ str"," ++ int j ++ str")"
+ str"Constr(" ++ pr_mind sp ++ str"," ++ int i ++ str"," ++ int j ++ str")"
| Case (ci,p,c,bl) -> v 0
(hv 0 (str"<"++pr_constr p++str">"++ cut() ++ str"Case " ++
pr_constr c ++ str"of") ++ cut() ++
@@ -729,7 +729,7 @@ let hdchar env c =
lowercase_first_char (id_of_label (con_label kn))
| Ind ((kn,i) as x) ->
if i=0 then
- lowercase_first_char (id_of_label (label kn))
+ lowercase_first_char (id_of_label (mind_label kn))
else
lowercase_first_char (basename_of_global (IndRef x))
| Construct ((sp,i) as x) ->
@@ -825,15 +825,22 @@ let names_of_rel_context env =
(**** Globality of identifiers *)
-let rec is_imported_modpath = function
- | MPfile dp -> true
- | p -> false
+let rec is_imported_modpath mp =
+ let current_mp,_ = Lib.current_prefix() in
+ match mp with
+ | MPfile dp ->
+ let rec find_prefix = function
+ |MPfile dp1 -> not (dp1=dp)
+ |MPdot(mp,_) -> find_prefix mp
+ |MPbound(_) -> false
+ in find_prefix current_mp
+ | p -> false
let is_imported_ref = function
| VarRef _ -> false
| IndRef (kn,_)
| ConstructRef ((kn,_),_) ->
- let (mp,_,_) = repr_kn kn in is_imported_modpath mp
+ let (mp,_,_) = repr_mind kn in is_imported_modpath mp
| ConstRef kn ->
let (mp,_,_) = repr_con kn in is_imported_modpath mp
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index 9d35225737..539821403d 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -111,7 +111,7 @@ let load_class (_, cl) =
let cache_class = load_class
-let subst_class (_,subst,cl) =
+let subst_class (subst,cl) =
let do_subst_con c = fst (Mod_subst.subst_con subst c)
and do_subst c = Mod_subst.subst_mps subst c
and do_subst_gr gr = fst (subst_global subst gr) in
@@ -187,8 +187,9 @@ let load_instance (_,inst) =
instances := Gmap.add inst.is_class insts !instances
let cache_instance = load_instance
-let subst_instance (_,subst,inst) =
- { inst with
+
+let subst_instance (subst,inst) =
+ { inst with
is_class = fst (subst_global subst inst.is_class);
is_impl = fst (Mod_subst.subst_con subst inst.is_impl) }
generated by cgit v1.2.3 (git 2.25.1) at 2026-09-27 09:02:04 +0000