aboutsummaryrefslogtreecommitdiff
path: root/engine
diff options
context:
space:
mode:
Diffstat (limited to 'engine')
-rw-r--r--engine/eConstr.ml55
-rw-r--r--engine/eConstr.mli9
-rw-r--r--engine/evarutil.ml34
-rw-r--r--engine/evarutil.mli25
-rw-r--r--engine/evd.ml3
-rw-r--r--engine/evd.mli2
-rw-r--r--engine/namegen.ml5
-rw-r--r--engine/termops.ml32
-rw-r--r--engine/univProblem.ml2
-rw-r--r--engine/univSubst.ml13
10 files changed, 88 insertions, 92 deletions
diff --git a/engine/eConstr.ml b/engine/eConstr.ml
index 42c9359ff0..334c23c963 100644
--- a/engine/eConstr.ml
+++ b/engine/eConstr.ml
@@ -69,7 +69,7 @@ let mkInd i = of_kind (Ind (in_punivs i))
let mkConstructU pc = of_kind (Construct pc)
let mkConstruct c = of_kind (Construct (in_punivs c))
let mkConstructUi ((ind,u),i) = of_kind (Construct ((ind,i),u))
-let mkCase (ci, c, r, p) = of_kind (Case (ci, c, r, p))
+let mkCase (ci, c, iv, r, p) = of_kind (Case (ci, c, iv, r, p))
let mkFix f = of_kind (Fix f)
let mkCoFix f = of_kind (CoFix f)
let mkProj (p, c) = of_kind (Proj (p, c))
@@ -77,6 +77,7 @@ let mkArrow t1 r t2 = of_kind (Prod (make_annot Anonymous r, t1, t2))
let mkArrowR t1 t2 = mkArrow t1 Sorts.Relevant t2
let mkInt i = of_kind (Int i)
let mkFloat f = of_kind (Float f)
+let mkArray (u,t,def,ty) = of_kind (Array (u,t,def,ty))
let mkRef (gr,u) = let open GlobRef in match gr with
| ConstRef c -> mkConstU (c,u)
@@ -194,7 +195,7 @@ let destCoFix sigma c = match kind sigma c with
| _ -> raise DestKO
let destCase sigma c = match kind sigma c with
-| Case (ci, t, c, p) -> (ci, t, c, p)
+| Case (ci, t, iv, c, p) -> (ci, t, iv, c, p)
| _ -> raise DestKO
let destProj sigma c = match kind sigma c with
@@ -356,7 +357,7 @@ let iter_with_full_binders sigma g f n c =
| LetIn (na,b,t,c) -> f n b; f n t; f (g (LocalDef (na, b, t)) n) c
| App (c,l) -> f n c; Array.Fun1.iter f n l
| Evar (_,l) -> List.iter (fun c -> f n c) l
- | Case (_,p,c,bl) -> f n p; f n c; Array.Fun1.iter f n bl
+ | Case (_,p,iv,c,bl) -> f n p; iter_invert (f n) iv; f n c; Array.Fun1.iter f n bl
| Proj (p,c) -> f n c
| Fix (_,(lna,tl,bl)) ->
Array.iter (f n) tl;
@@ -366,6 +367,7 @@ let iter_with_full_binders sigma g f n c =
Array.iter (f n) tl;
let n' = Array.fold_left2_i (fun i n na t -> g (LocalAssum (na,lift i t)) n) n lna tl in
Array.iter (f n') bl
+ | Array (_u,t,def,ty) -> Array.Fun1.iter f n t; f n def; f n ty
let iter_with_binders sigma g f n c =
let f l c = f l (of_constr c) in
@@ -380,7 +382,7 @@ let compare_gen k eq_inst eq_sort eq_constr nargs c1 c2 =
let eq_constr sigma c1 c2 =
let kind c = kind sigma c in
- let eq_inst _ _ i1 i2 = EInstance.equal sigma i1 i2 in
+ let eq_inst _ i1 i2 = EInstance.equal sigma i1 i2 in
let eq_sorts s1 s2 = ESorts.equal sigma s1 s2 in
let rec eq_constr nargs c1 c2 =
compare_gen kind eq_inst eq_sorts eq_constr nargs c1 c2
@@ -390,13 +392,13 @@ let eq_constr sigma c1 c2 =
let eq_constr_nounivs sigma c1 c2 =
let kind c = kind sigma c in
let rec eq_constr nargs c1 c2 =
- compare_gen kind (fun _ _ _ _ -> true) (fun _ _ -> true) eq_constr nargs c1 c2
+ compare_gen kind (fun _ _ _ -> true) (fun _ _ -> true) eq_constr nargs c1 c2
in
eq_constr 0 c1 c2
let compare_constr sigma cmp c1 c2 =
let kind c = kind sigma c in
- let eq_inst _ _ i1 i2 = EInstance.equal sigma i1 i2 in
+ let eq_inst _ i1 i2 = EInstance.equal sigma i1 i2 in
let eq_sorts s1 s2 = ESorts.equal sigma s1 s2 in
let cmp nargs c1 c2 = cmp c1 c2 in
compare_gen kind eq_inst eq_sorts cmp 0 c1 c2
@@ -442,22 +444,22 @@ let cmp_constructors (mind, ind, cns as spec) nargs u1 u2 cstrs =
Array.fold_left2 (fun cstrs u1 u2 -> UnivProblem.(Set.add (UWeak (u1,u2)) cstrs))
cstrs (Univ.Instance.to_array u1) (Univ.Instance.to_array u2)
-let eq_universes env sigma cstrs cv_pb ref nargs l l' =
+let eq_universes env sigma cstrs cv_pb refargs l l' =
if EInstance.is_empty l then (assert (EInstance.is_empty l'); true)
else
let l = EInstance.kind sigma l
and l' = EInstance.kind sigma l' in
let open GlobRef in
let open UnivProblem in
- match ref with
- | VarRef _ -> assert false (* variables don't have instances *)
- | ConstRef _ ->
+ match refargs with
+ | None | Some (ConstRef _, _) ->
cstrs := enforce_eq_instances_univs true l l' !cstrs; true
- | IndRef ind ->
+ | Some (VarRef _, _) -> assert false (* variables don't have instances *)
+ | Some (IndRef ind, nargs) ->
let mind = Environ.lookup_mind (fst ind) env in
cstrs := cmp_inductives cv_pb (mind,snd ind) nargs l l' !cstrs;
true
- | ConstructRef ((mi,ind),ctor) ->
+ | Some (ConstructRef ((mi,ind),ctor), nargs) ->
let mind = Environ.lookup_mind mi env in
cstrs := cmp_constructors (mind,ind,ctor) nargs l l' !cstrs;
true
@@ -469,8 +471,8 @@ let test_constr_universes env sigma leq m n =
else
let cstrs = ref Set.empty in
let cv_pb = if leq then Reduction.CUMUL else Reduction.CONV in
- let eq_universes ref nargs l l' = eq_universes env sigma cstrs Reduction.CONV ref nargs l l'
- and leq_universes ref nargs l l' = eq_universes env sigma cstrs cv_pb ref nargs l l' in
+ let eq_universes refargs l l' = eq_universes env sigma cstrs Reduction.CONV refargs l l'
+ and leq_universes refargs l l' = eq_universes env sigma cstrs cv_pb refargs l l' in
let eq_sorts s1 s2 =
let s1 = ESorts.kind sigma s1 in
let s2 = ESorts.kind sigma s2 in
@@ -546,18 +548,21 @@ let universes_of_constr sigma c =
let rec aux s c =
match kind sigma c with
| Const (c, u) ->
- LSet.fold LSet.add (Instance.levels (EInstance.kind sigma u)) s
+ LSet.fold LSet.add (Instance.levels (EInstance.kind sigma u)) s
| Ind ((mind,_), u) | Construct (((mind,_),_), u) ->
- LSet.fold LSet.add (Instance.levels (EInstance.kind sigma u)) s
+ LSet.fold LSet.add (Instance.levels (EInstance.kind sigma u)) s
| Sort u ->
- let sort = ESorts.kind sigma u in
- if Sorts.is_small sort then s
- else
- let u = Sorts.univ_of_sort sort in
- LSet.fold LSet.add (Universe.levels u) s
+ let sort = ESorts.kind sigma u in
+ if Sorts.is_small sort then s
+ else
+ let u = Sorts.univ_of_sort sort in
+ LSet.fold LSet.add (Universe.levels u) s
| Evar (k, args) ->
- let concl = Evd.evar_concl (Evd.find sigma k) in
- fold sigma aux (aux s concl) c
+ let concl = Evd.evar_concl (Evd.find sigma k) in
+ fold sigma aux (aux s concl) c
+ | Array (u,_,_,_) ->
+ let s = LSet.fold LSet.add (Instance.levels (EInstance.kind sigma u)) s in
+ fold sigma aux s c
| _ -> fold sigma aux s c
in aux LSet.empty c
@@ -762,7 +767,7 @@ let kind_of_type sigma t = match kind sigma t with
| (Rel _ | Meta _ | Var _ | Evar _ | Const _
| Proj _ | Case _ | Fix _ | CoFix _ | Ind _)
-> AtomicType (t,[||])
- | (Lambda _ | Construct _ | Int _ | Float _) -> failwith "Not a type"
+ | (Lambda _ | Construct _ | Int _ | Float _ | Array _) -> failwith "Not a type"
module Unsafe =
struct
@@ -777,5 +782,7 @@ let to_named_context =
= fun Refl x -> x
in
gen unsafe_eq
+let to_case_invert = unsafe_to_case_invert
+
let eq = unsafe_eq
end
diff --git a/engine/eConstr.mli b/engine/eConstr.mli
index aea441b90b..d0f675319d 100644
--- a/engine/eConstr.mli
+++ b/engine/eConstr.mli
@@ -128,13 +128,14 @@ val mkIndU : inductive * EInstance.t -> t
val mkConstruct : constructor -> t
val mkConstructU : constructor * EInstance.t -> t
val mkConstructUi : (inductive * EInstance.t) * int -> t
-val mkCase : case_info * t * t * t array -> t
+val mkCase : case_info * t * (t,EInstance.t) case_invert * t * t array -> t
val mkFix : (t, t) pfixpoint -> t
val mkCoFix : (t, t) pcofixpoint -> t
val mkArrow : t -> Sorts.relevance -> t -> t
val mkArrowR : t -> t -> t
val mkInt : Uint63.t -> t
val mkFloat : Float64.t -> t
+val mkArray : EInstance.t * t array * t * t -> t
val mkRef : GlobRef.t * EInstance.t -> t
@@ -198,7 +199,7 @@ val destConst : Evd.evar_map -> t -> Constant.t * EInstance.t
val destEvar : Evd.evar_map -> t -> t pexistential
val destInd : Evd.evar_map -> t -> inductive * EInstance.t
val destConstruct : Evd.evar_map -> t -> constructor * EInstance.t
-val destCase : Evd.evar_map -> t -> case_info * t * t * t array
+val destCase : Evd.evar_map -> t -> case_info * t * (t,EInstance.t) case_invert * t * t array
val destProj : Evd.evar_map -> t -> Projection.t * t
val destFix : Evd.evar_map -> t -> (t, t) pfixpoint
val destCoFix : Evd.evar_map -> t -> (t, t) pcofixpoint
@@ -341,6 +342,8 @@ val of_rel_decl : (Constr.t, Constr.types) Context.Rel.Declaration.pt -> (t, typ
val to_rel_decl : Evd.evar_map -> (t, types) Context.Rel.Declaration.pt -> (Constr.t, Constr.types) Context.Rel.Declaration.pt
+val of_case_invert : (Constr.t,Univ.Instance.t) case_invert -> (t,EInstance.t) case_invert
+
(** {5 Unsafe operations} *)
module Unsafe :
@@ -365,6 +368,8 @@ sig
val to_instance : EInstance.t -> Univ.Instance.t
(** Physical identity. Does not care for normalization. *)
+ val to_case_invert : (t,EInstance.t) case_invert -> (Constr.t,Univ.Instance.t) case_invert
+
val eq : (t, Constr.t) eq
(** Use for transparent cast between types. *)
end
diff --git a/engine/evarutil.ml b/engine/evarutil.ml
index 0db9f498b9..b4b2032dd2 100644
--- a/engine/evarutil.ml
+++ b/engine/evarutil.ml
@@ -144,7 +144,7 @@ let head_evar sigma c =
let c = EConstr.Unsafe.to_constr c in
let rec hrec c = match kind c with
| Evar (evk,_) -> evk
- | Case (_,_,c,_) -> hrec c
+ | Case (_,_,_,c,_) -> hrec c
| App (c,_) -> hrec c
| Cast (c,_,_) -> hrec c
| Proj (p, c) -> hrec c
@@ -409,15 +409,8 @@ let push_rel_context_to_named_context ?hypnaming env sigma typ =
let default_source = Loc.tag @@ Evar_kinds.InternalHole
-let new_pure_evar_full evd ?typeclass_candidate evi =
- let (evd, evk) = Evd.new_evar evd ?typeclass_candidate evi in
- let evd = Evd.declare_future_goal evk evd in
- (evd, evk)
-
-let new_pure_evar?(src=default_source) ?(filter = Filter.identity) ?(abstract_arguments = Abstraction.identity)
- ?candidates ?naming ?typeclass_candidate ?(principal=false) sign evd typ =
- let default_naming = IntroAnonymous in
- let naming = Option.default default_naming naming in
+let new_pure_evar ?(src=default_source) ?(filter = Filter.identity) ?(abstract_arguments = Abstraction.identity)
+ ?candidates ?(naming = IntroAnonymous) ?typeclass_candidate ?(principal=false) sign evd typ =
let name = match naming with
| IntroAnonymous -> None
| IntroIdentifier id -> Some id
@@ -443,22 +436,6 @@ let new_pure_evar?(src=default_source) ?(filter = Filter.identity) ?(abstract_ar
in
(evd, newevk)
-let new_evar_instance ?src ?filter ?abstract_arguments ?candidates ?naming ?typeclass_candidate
- ?principal sign evd typ instance =
- let open EConstr in
- assert (not !Flags.debug ||
- List.distinct (ids_of_named_context (named_context_of_val sign)));
- let (evd, newevk) = new_pure_evar sign evd ?src ?filter ?abstract_arguments ?candidates ?naming ?typeclass_candidate ?principal typ in
- evd, mkEvar (newevk, instance)
-
-let new_evar_from_context ?src ?filter ?candidates ?naming ?typeclass_candidate ?principal sign evd typ =
- let instance = List.map (NamedDecl.get_id %> EConstr.mkVar) (named_context_of_val sign) in
- let instance =
- match filter with
- | None -> instance
- | Some filter -> Filter.filter_list filter instance in
- new_evar_instance sign evd typ ?src ?filter ?candidates ?naming ?principal instance
-
(* [new_evar] declares a new existential in an env env with type typ *)
(* Converting the env into the sign of the evar to define *)
let new_evar ?src ?filter ?abstract_arguments ?candidates ?naming ?typeclass_candidate
@@ -470,8 +447,9 @@ let new_evar ?src ?filter ?abstract_arguments ?candidates ?naming ?typeclass_can
match filter with
| None -> instance
| Some filter -> Filter.filter_list filter instance in
- new_evar_instance sign evd typ' ?src ?filter ?abstract_arguments ?candidates ?naming
- ?typeclass_candidate ?principal instance
+ let (evd, evk) = new_pure_evar sign evd typ' ?src ?filter ?abstract_arguments ?candidates ?naming
+ ?typeclass_candidate ?principal in
+ (evd, EConstr.mkEvar (evk, instance))
let new_type_evar ?src ?filter ?naming ?principal ?hypnaming env evd rigid =
let (evd', s) = new_sort_variable rigid evd in
diff --git a/engine/evarutil.mli b/engine/evarutil.mli
index b3c94e6b3b..41b58d38b0 100644
--- a/engine/evarutil.mli
+++ b/engine/evarutil.mli
@@ -25,14 +25,6 @@ val mk_new_meta : unit -> constr
(** {6 Creating a fresh evar given their type and context} *)
-val new_evar_from_context :
- ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t ->
- ?candidates:constr list ->
- ?naming:intro_pattern_naming_expr ->
- ?typeclass_candidate:bool ->
- ?principal:bool ->
- named_context_val -> evar_map -> types -> evar_map * EConstr.t
-
type naming_mode =
| KeepUserNameAndRenameExistingButSectionNames
| KeepUserNameAndRenameExistingEvenSectionNames
@@ -56,8 +48,6 @@ val new_pure_evar :
?principal:bool ->
named_context_val -> evar_map -> types -> evar_map * Evar.t
-val new_pure_evar_full : evar_map -> ?typeclass_candidate:bool -> evar_info -> evar_map * Evar.t
-
(** Create a new Type existential variable, as we keep track of
them during type-checking and unification. *)
val new_type_evar :
@@ -73,21 +63,6 @@ val new_Type : ?rigid:rigid -> evar_map -> evar_map * constr
val new_global : evar_map -> GlobRef.t -> evar_map * constr
-(** Create a fresh evar in a context different from its definition context:
- [new_evar_instance sign evd ty inst] creates a new evar of context
- [sign] and type [ty], [inst] is a mapping of the evar context to
- the context where the evar should occur. This means that the terms
- of [inst] are typed in the occurrence context and their type (seen
- as a telescope) is [sign] *)
-val new_evar_instance :
- ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t ->
- ?abstract_arguments:Abstraction.t -> ?candidates:constr list ->
- ?naming:intro_pattern_naming_expr ->
- ?typeclass_candidate:bool ->
- ?principal:bool ->
- named_context_val -> evar_map -> types ->
- constr list -> evar_map * constr
-
val make_pure_subst : evar_info -> 'a list -> (Id.t * 'a) list
val safe_evar_value : evar_map -> Constr.existential -> Constr.constr option
diff --git a/engine/evd.ml b/engine/evd.ml
index f0ee8ae68f..c570f75c6b 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -1398,6 +1398,9 @@ module MiniEConstr = struct
let unsafe_to_rel_decl d = d
let to_rel_decl sigma d = Context.Rel.Declaration.map_constr (to_constr sigma) d
+ let unsafe_to_case_invert x = x
+ let of_case_invert x = x
+
end
(** The following functions return the set of evars immediately
diff --git a/engine/evd.mli b/engine/evd.mli
index d9b7bd76e7..679173ca72 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -732,6 +732,8 @@ module MiniEConstr : sig
(Constr.t, Constr.types) Context.Named.Declaration.pt
val unsafe_to_rel_decl : (t, t) Context.Rel.Declaration.pt ->
(Constr.t, Constr.types) Context.Rel.Declaration.pt
+ val of_case_invert : (constr,Univ.Instance.t) case_invert -> (econstr,EInstance.t) case_invert
+ val unsafe_to_case_invert : (econstr,EInstance.t) case_invert -> (constr,Univ.Instance.t) case_invert
val of_rel_decl : (Constr.t, Constr.types) Context.Rel.Declaration.pt ->
(t, t) Context.Rel.Declaration.pt
val to_rel_decl : evar_map -> (t, t) Context.Rel.Declaration.pt ->
diff --git a/engine/namegen.ml b/engine/namegen.ml
index c4472050f8..fb9f6db0ea 100644
--- a/engine/namegen.ml
+++ b/engine/namegen.ml
@@ -118,7 +118,7 @@ let head_name sigma c = (* Find the head constant of a constr if any *)
Some (Nametab.basename_of_global (global_of_constr c))
| Fix ((_,i),(lna,_,_)) | CoFix (i,(lna,_,_)) ->
Some (match lna.(i).binder_name with Name id -> id | _ -> assert false)
- | Sort _ | Rel _ | Meta _|Evar _|Case (_, _, _, _) | Int _ | Float _ -> None
+ | Sort _ | Rel _ | Meta _|Evar _|Case _ | Int _ | Float _ | Array _ -> None
in
hdrec c
@@ -163,9 +163,10 @@ let hdchar env sigma c =
let id = match lna.(i).binder_name with Name id -> id | _ -> assert false in
lowercase_first_char id
| Evar _ (* We could do better... *)
- | Meta _ | Case (_, _, _, _) -> "y"
+ | Meta _ | Case _ -> "y"
| Int _ -> "i"
| Float _ -> "f"
+ | Array _ -> "a"
in
hdrec 0 c
diff --git a/engine/termops.ml b/engine/termops.ml
index c51e753d46..e5231ef9cd 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -639,13 +639,14 @@ let map_constr_with_binders_left_to_right sigma g f l c =
let al' = List.map_left (f l) al in
if List.for_all2 (==) al' al then c
else mkEvar (e, al')
- | Case (ci,p,b,bl) ->
+ | Case (ci,p,iv,b,bl) ->
(* In v8 concrete syntax, predicate is after the term to match! *)
let b' = f l b in
+ let iv' = map_invert (f l) iv in
let p' = f l p in
let bl' = Array.map_left (f l) bl in
- if b' == b && p' == p && bl' == bl then c
- else mkCase (ci, p', b', bl')
+ if b' == b && p' == p && iv' == iv && bl' == bl then c
+ else mkCase (ci, p', iv', b', bl')
| Fix (ln,(lna,tl,bl as fx)) ->
let l' = fold_rec_types g fx l in
let (tl', bl') = map_left2 (f l) tl (f l') bl in
@@ -658,6 +659,12 @@ let map_constr_with_binders_left_to_right sigma g f l c =
if Array.for_all2 (==) tl tl' && Array.for_all2 (==) bl bl'
then c
else mkCoFix (ln,(lna,tl',bl'))
+ | Array(u,t,def,ty) ->
+ let t' = Array.map_left (f l) t in
+ let def' = f l def in
+ let ty' = f l ty in
+ if def' == def && t' == t && ty' == ty then c
+ else mkArray(u,t',def',ty')
let map_under_context_with_full_binders sigma g f l n d =
let open EConstr in
@@ -709,18 +716,20 @@ let map_constr_with_full_binders_gen userview sigma g f l cstr =
| Evar (e,al) ->
let al' = List.map (f l) al in
if List.for_all2 (==) al al' then cstr else mkEvar (e, al')
- | Case (ci,p,c,bl) when userview ->
+ | Case (ci,p,iv,c,bl) when userview ->
let p' = map_return_predicate_with_full_binders sigma g f l ci p in
+ let iv' = map_invert (f l) iv in
let c' = f l c in
let bl' = map_branches_with_full_binders sigma g f l ci bl in
- if p==p' && c==c' && bl'==bl then cstr else
- mkCase (ci, p', c', bl')
- | Case (ci,p,c,bl) ->
+ if p==p' && iv'==iv && c==c' && bl'==bl then cstr else
+ mkCase (ci, p', iv', c', bl')
+ | Case (ci,p,iv,c,bl) ->
let p' = f l p in
+ let iv' = map_invert (f l) iv in
let c' = f l c in
let bl' = Array.map (f l) bl in
- if p==p' && c==c' && Array.for_all2 (==) bl bl' then cstr else
- mkCase (ci, p', c', bl')
+ if p==p' && iv'==iv && c==c' && Array.for_all2 (==) bl bl' then cstr else
+ mkCase (ci, p', iv', c', bl')
| Fix (ln,(lna,tl,bl as fx)) ->
let tl' = Array.map (f l) tl in
let l' = fold_rec_types g fx l in
@@ -735,6 +744,11 @@ let map_constr_with_full_binders_gen userview sigma g f l cstr =
if Array.for_all2 (==) tl tl' && Array.for_all2 (==) bl bl'
then cstr
else mkCoFix (ln,(lna,tl',bl'))
+ | Array(u,t,def,ty) ->
+ let t' = Array.Smart.map (f l) t in
+ let def' = f l def in
+ let ty' = f l ty in
+ if def==def' && t == t' && ty==ty' then cstr else mkArray (u,t', def',ty')
let map_constr_with_full_binders sigma g f =
map_constr_with_full_binders_gen false sigma g f
diff --git a/engine/univProblem.ml b/engine/univProblem.ml
index 08ff9efa5b..8d6689933c 100644
--- a/engine/univProblem.ml
+++ b/engine/univProblem.ml
@@ -150,7 +150,7 @@ let eq_constr_univs_infer_with kind1 kind2 univs fold m n accu =
[kind1,kind2], because [kind1] and [kind2] may be different,
typically evaluating [m] and [n] in different evar maps. *)
let cstrs = ref accu in
- let eq_universes _ _ = UGraph.check_eq_instances univs in
+ let eq_universes _ = UGraph.check_eq_instances univs in
let eq_sorts s1 s2 =
if Sorts.equal s1 s2 then true
else
diff --git a/engine/univSubst.ml b/engine/univSubst.ml
index 92211d5f3d..335c2e5e68 100644
--- a/engine/univSubst.ml
+++ b/engine/univSubst.ml
@@ -146,7 +146,18 @@ let nf_evars_and_universes_opt_subst f subst =
if pu' == pu then c else mkConstructU pu'
| Sort (Type u) ->
let u' = Univ.subst_univs_universe subst u in
- if u' == u then c else mkSort (sort_of_univ u')
+ if u' == u then c else mkSort (sort_of_univ u')
+ | Case (ci,p,CaseInvert {univs;args},t,br) ->
+ let univs' = Instance.subst_fn lsubst univs in
+ if univs' == univs then Constr.map aux c
+ else Constr.map aux (mkCase (ci,p,CaseInvert {univs=univs';args},t,br))
+ | Array (u,elems,def,ty) ->
+ let u' = Univ.Instance.subst_fn lsubst u in
+ let elems' = CArray.Smart.map aux elems in
+ let def' = aux def in
+ let ty' = aux ty in
+ if u == u' && elems == elems' && def == def' && ty == ty' then c
+ else mkArray (u',elems',def',ty')
| _ -> Constr.map aux c
in aux
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-29 12:56:45 +0000