aboutsummaryrefslogtreecommitdiff
path: root/pretyping
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping')
-rw-r--r--pretyping/cases.ml4
-rw-r--r--pretyping/coercion.ml2
-rw-r--r--pretyping/detyping.ml42
-rw-r--r--pretyping/evarconv.ml16
-rw-r--r--pretyping/glob_ops.ml22
-rw-r--r--pretyping/glob_ops.mli1
-rw-r--r--pretyping/inductiveops.ml49
-rw-r--r--pretyping/inductiveops.mli8
-rw-r--r--pretyping/inferCumulativity.ml44
-rw-r--r--pretyping/inferCumulativity.mli2
-rw-r--r--pretyping/nativenorm.ml3
-rw-r--r--pretyping/pretyping.ml13
-rw-r--r--pretyping/typing.ml6
-rw-r--r--pretyping/vnorm.ml3
14 files changed, 79 insertions, 136 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index ed7c3d6770..1ad90b2953 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -426,7 +426,7 @@ let adjust_tomatch_to_pattern ~program_mode sigma pb ((current,typ),deps,dep) =
let tm1 = List.map (fun eqn -> List.hd eqn.patterns) pb.mat in
(match find_row_ind tm1 with
| None -> sigma, (current, tmtyp)
- | Some (_,(ind,_)) ->
+ | Some (loc,(ind,_)) ->
let sigma, indt = inductive_template !!(pb.env) sigma None ind in
let sigma, current =
if List.is_empty deps && isEvar sigma typ then
@@ -435,7 +435,7 @@ let adjust_tomatch_to_pattern ~program_mode sigma pb ((current,typ),deps,dep) =
| None -> sigma, current
| Some sigma -> sigma, current
else
- let sigma, j = Coercion.inh_conv_coerce_to ~program_mode true !!(pb.env) sigma (make_judge current typ) indt in
+ let sigma, j = Coercion.inh_conv_coerce_to ?loc ~program_mode true !!(pb.env) sigma (make_judge current typ) indt in
sigma, j.uj_val
in
sigma, (current, try_find_ind !!(pb.env) sigma indt names))
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index 9e93c470b1..2329b87acc 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -434,7 +434,7 @@ let inh_tosort_force ?loc env evd j =
try
let t,p = lookup_path_to_sort_from env evd j.uj_type in
let evd,j1 = apply_coercion env evd p j t in
- let j2 = on_judgment_type (whd_evar evd) j1 in
+ let j2 = Environ.on_judgment_type (whd_evar evd) j1 in
(evd,type_judgment env evd j2)
with Not_found | NoCoercion ->
error_not_a_type ?loc env evd j
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 6746e4b902..99cd89cc2a 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -8,8 +8,6 @@
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
-module CVars = Vars
-
open Pp
open CErrors
open Util
@@ -175,16 +173,6 @@ let () = declare_bool_option
optread = print_primproj_params;
optwrite = (:=) print_primproj_params_value }
-let print_primproj_compatibility_value = ref false
-let print_primproj_compatibility () = !print_primproj_compatibility_value
-
-let () = declare_bool_option
- { optdepr = false;
- optname = "backwards-compatible printing of primitive projections";
- optkey = ["Printing";"Primitive";"Projection";"Compatibility"];
- optread = print_primproj_compatibility;
- optwrite = (:=) print_primproj_compatibility_value }
-
(* Auxiliary function for MutCase printing *)
(* [computable] tries to tell if the predicate typing the result is inferable*)
@@ -702,30 +690,12 @@ and detype_r d flags avoid env sigma t =
GApp (DAst.make @@ GRef (ConstRef (Projection.constant p), None),
[detype d flags avoid env sigma c])
else
- if print_primproj_compatibility () && Projection.unfolded p then
- (* Print the compatibility match version *)
- let c' =
- try
- let ind = Projection.inductive p in
- let bodies = Inductiveops.legacy_match_projection (snd env) ind in
- let body = bodies.(Projection.arg p) in
- let ty = Retyping.get_type_of (snd env) sigma c in
- let ((ind,u), args) = Inductiveops.find_mrectype (snd env) sigma ty in
- let body' = strip_lam_assum body in
- let u = EInstance.kind sigma u in
- let body' = CVars.subst_instance_constr u body' in
- let body' = EConstr.of_constr body' in
- substl (c :: List.rev args) body'
- with Retyping.RetypeError _ | Not_found ->
- anomaly (str"Cannot detype an unfolded primitive projection.")
- in DAst.get (detype d flags avoid env sigma c')
- else
- if print_primproj_params () then
- try
- let c = Retyping.expand_projection (snd env) sigma p c [] in
- DAst.get (detype d flags avoid env sigma c)
- with Retyping.RetypeError _ -> noparams ()
- else noparams ()
+ if print_primproj_params () then
+ try
+ let c = Retyping.expand_projection (snd env) sigma p c [] in
+ DAst.get (detype d flags avoid env sigma c)
+ with Retyping.RetypeError _ -> noparams ()
+ else noparams ()
| Evar (evk,cl) ->
let bound_to_itself_or_letin decl c =
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index aa30ed8d2e..bb163ddaee 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -468,17 +468,16 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
let u = EInstance.kind evd u and u' = EInstance.kind evd u' in
let mind = Environ.lookup_mind mi env in
let open Declarations in
- begin match mind.mind_universes with
- | Monomorphic_ind _ -> assert false
- | Polymorphic_ind _ -> check_strict evd u u'
- | Cumulative_ind cumi ->
+ begin match mind.mind_variance with
+ | None -> check_strict evd u u'
+ | Some variances ->
let nparamsaplied = Stack.args_size sk in
let nparamsaplied' = Stack.args_size sk' in
let needed = Reduction.inductive_cumulativity_arguments (mind,i) in
if not (Int.equal nparamsaplied needed && Int.equal nparamsaplied' needed)
then check_strict evd u u'
else
- compare_cumulative_instances evd (Univ.ACumulativityInfo.variance cumi) u u'
+ compare_cumulative_instances evd variances u u'
end
| Ind _, Ind _ -> UnifFailure (evd, NotSameHead)
| Construct (((mi,ind),ctor as cons), u), Construct (cons', u')
@@ -488,10 +487,9 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
let u = EInstance.kind evd u and u' = EInstance.kind evd u' in
let mind = Environ.lookup_mind mi env in
let open Declarations in
- begin match mind.mind_universes with
- | Monomorphic_ind _ -> assert false
- | Polymorphic_ind _ -> check_strict evd u u'
- | Cumulative_ind cumi ->
+ begin match mind.mind_variance with
+ | None -> check_strict evd u u'
+ | Some variances ->
let nparamsaplied = Stack.args_size sk in
let nparamsaplied' = Stack.args_size sk' in
let needed = Reduction.constructor_cumulativity_arguments (mind,ind,ctor) in
diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml
index 6b61b1452e..affed5389f 100644
--- a/pretyping/glob_ops.ml
+++ b/pretyping/glob_ops.ml
@@ -485,7 +485,11 @@ let is_gvar id c = match DAst.get c with
| GVar id' -> Id.equal id id'
| _ -> false
-let rec cases_pattern_of_glob_constr na = DAst.map (function
+let rec cases_pattern_of_glob_constr na c =
+ (* Forcing evaluation to ensure that the possible raising of
+ Not_found is not delayed *)
+ let c = DAst.force c in
+ DAst.map (function
| GVar id ->
begin match na with
| Name _ ->
@@ -498,6 +502,8 @@ let rec cases_pattern_of_glob_constr na = DAst.map (function
| GApp (c, l) ->
begin match DAst.get c with
| GRef (ConstructRef cstr,_) ->
+ let nparams = Inductiveops.inductive_nparams (fst cstr) in
+ let _,l = List.chop nparams l in
PatCstr (cstr,List.map (cases_pattern_of_glob_constr Anonymous) l,na)
| _ -> raise Not_found
end
@@ -505,15 +511,14 @@ let rec cases_pattern_of_glob_constr na = DAst.map (function
(* A canonical encoding of aliases *)
DAst.get (cases_pattern_of_glob_constr na' b)
| _ -> raise Not_found
- )
+ ) c
open Declarations
-open Term
open Context
(* Keep only patterns which are not bound to a local definitions *)
-let drop_local_defs typi args =
- let (decls,_) = decompose_prod_assum typi in
+let drop_local_defs params decls args =
+ let decls = List.skipn (Rel.length params) (List.rev decls) in
let rec aux decls args =
match decls, args with
| [], [] -> []
@@ -525,7 +530,7 @@ let drop_local_defs typi args =
end
| Rel.Declaration.LocalAssum _ :: decls, a :: args -> a :: aux decls args
| _ -> assert false in
- aux (List.rev decls) args
+ aux decls args
let add_patterns_for_params_remove_local_defs (ind,j) l =
let (mib,mip) = Global.lookup_inductive ind in
@@ -534,9 +539,8 @@ let add_patterns_for_params_remove_local_defs (ind,j) l =
if mip.mind_consnrealdecls.(j-1) = mip.mind_consnrealargs.(j-1) then
(* Optimisation *) l
else
- let typi = mip.mind_nf_lc.(j-1) in
- let (_,typi) = decompose_prod_n_assum (Rel.length mib.mind_params_ctxt) typi in
- drop_local_defs typi l in
+ let (ctx, _) = mip.mind_nf_lc.(j - 1) in
+ drop_local_defs mib.mind_params_ctxt ctx l in
Util.List.addn nparams (DAst.make @@ PatVar Anonymous) l
let add_alias ?loc na c =
diff --git a/pretyping/glob_ops.mli b/pretyping/glob_ops.mli
index 91a2ef9c1e..c189a3bcb2 100644
--- a/pretyping/glob_ops.mli
+++ b/pretyping/glob_ops.mli
@@ -89,6 +89,7 @@ val map_pattern : (glob_constr -> glob_constr) ->
(** Conversion from glob_constr to cases pattern, if possible
+ Evaluation is forced.
Take the current alias as parameter,
@raise Not_found if translation is impossible *)
val cases_pattern_of_glob_constr : Name.t -> 'a glob_constr_g -> 'a cases_pattern_g
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index ff552c7caf..d937456bcb 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -101,7 +101,8 @@ let mis_nf_constructor_type ((ind,u),mib,mip) j =
and nconstr = Array.length mip.mind_consnames in
let make_Ik k = mkIndU (((fst ind),ntypes-k-1),u) in
if j > nconstr then user_err Pp.(str "Not enough constructors in the type.");
- substl (List.init ntypes make_Ik) (subst_instance_constr u specif.(j-1))
+ let (ctx, cty) = specif.(j - 1) in
+ substl (List.init ntypes make_Ik) (subst_instance_constr u (Term.it_mkProd_or_LetIn cty ctx))
(* Number of constructors *)
@@ -280,8 +281,7 @@ let make_case_info env ind style =
let ind_tags =
Context.Rel.to_tags (List.firstn mip.mind_nrealdecls mip.mind_arity_ctxt) in
let cstr_tags =
- Array.map2 (fun c n ->
- let d,_ = decompose_prod_assum c in
+ Array.map2 (fun (d, _) n ->
Context.Rel.to_tags (List.firstn n d))
mip.mind_nf_lc mip.mind_consnrealdecls in
let print_info = { ind_tags; cstr_tags; style } in
@@ -453,12 +453,7 @@ let build_branch_type env sigma dep p cs =
let compute_projections env (kn, i as ind) =
let open Term in
let mib = Environ.lookup_mind kn env in
- let u = match mib.mind_universes with
- | Monomorphic_ind _ -> Instance.empty
- | Polymorphic_ind auctx -> make_abstract_instance auctx
- | Cumulative_ind acumi ->
- make_abstract_instance (ACumulativityInfo.univ_context acumi)
- in
+ let u = make_abstract_instance (Declareops.inductive_polymorphic_context mib) in
let x = match mib.mind_record with
| NotRecord | FakeRecord ->
anomaly Pp.(str "Trying to build primitive projections for a non-primitive record")
@@ -467,7 +462,8 @@ let compute_projections env (kn, i as ind) =
let pkt = mib.mind_packets.(i) in
let { mind_nparams = nparamargs; mind_params_ctxt = params } = mib in
let subst = List.init mib.mind_ntypes (fun i -> mkIndU ((kn, mib.mind_ntypes - i - 1), u)) in
- let rctx, _ = decompose_prod_assum (substl subst pkt.mind_nf_lc.(0)) in
+ let ctx, cty = pkt.mind_nf_lc.(0) in
+ let rctx, _ = decompose_prod_assum (substl subst (Term.it_mkProd_or_LetIn cty ctx)) in
let ctx, paramslet = List.chop pkt.mind_consnrealdecls.(0) rctx in
(* We build a substitution smashing the lets in the record parameters so
that typechecking projections requires just a substitution and not
@@ -480,25 +476,6 @@ let compute_projections env (kn, i as ind) =
(* [Ind inst] is typed in context [params-wo-let] *)
ty
in
- let ci =
- let print_info =
- { ind_tags = []; cstr_tags = [|Context.Rel.to_tags ctx|]; style = LetStyle } in
- { ci_ind = ind;
- ci_npar = nparamargs;
- ci_cstr_ndecls = pkt.mind_consnrealdecls;
- ci_cstr_nargs = pkt.mind_consnrealargs;
- ci_pp_info = print_info }
- in
- let len = List.length ctx in
- let compat_body ccl i =
- (* [ccl] is defined in context [params;x:indty] *)
- (* [ccl'] is defined in context [params;x:indty;x:indty] *)
- let ccl' = liftn 1 2 ccl in
- let p = mkLambda (x, lift 1 indty, ccl') in
- let branch = it_mkLambda_or_LetIn (mkRel (len - i)) ctx in
- let body = mkCase (ci, p, mkRel 1, [|lift 1 branch|]) in
- it_mkLambda_or_LetIn (mkLambda (x,indty,body)) params
- in
let projections decl (proj_arg, j, pbs, subst) =
match decl with
| LocalDef (na,c,t) ->
@@ -528,10 +505,9 @@ let compute_projections env (kn, i as ind) =
let ty = substl subst t in
let term = mkProj (Projection.make kn true, mkRel 1) in
let fterm = mkProj (Projection.make kn false, mkRel 1) in
- let compat = compat_body ty (j - 1) in
let etab = it_mkLambda_or_LetIn (mkLambda (x, indty, term)) params in
let etat = it_mkProd_or_LetIn (mkProd (x, indty, ty)) params in
- let body = (etab, etat, compat) in
+ let body = (etab, etat) in
(proj_arg + 1, j + 1, body :: pbs, fterm :: subst)
| Anonymous ->
anomaly Pp.(str "Trying to build primitive projections for a non-primitive record")
@@ -541,13 +517,6 @@ let compute_projections env (kn, i as ind) =
in
Array.rev_of_list pbs
-let legacy_match_projection env ind =
- Array.map pi3 (compute_projections env ind)
-
-let compute_projections ind mib =
- let ans = compute_projections ind mib in
- Array.map (fun (prj, ty, _) -> (prj, ty)) ans
-
(**************************************************)
let extract_mrectype sigma t =
@@ -654,9 +623,7 @@ let set_pattern_names env sigma ind brv =
let (mib,mip) = Inductive.lookup_mind_specif env ind in
let arities =
Array.map
- (fun c ->
- Context.Rel.length ((prod_assum c)) -
- mib.mind_nparams)
+ (fun (d, _) -> List.length d - mib.mind_nparams)
mip.mind_nf_lc in
Array.map2 (set_names env sigma) arities brv
diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli
index b2e205115f..5a4257e175 100644
--- a/pretyping/inductiveops.mli
+++ b/pretyping/inductiveops.mli
@@ -194,14 +194,6 @@ val compute_projections : Environ.env -> inductive -> (constr * types) array
(** Given a primitive record type, for every field computes the eta-expanded
projection and its type. *)
-val legacy_match_projection : Environ.env -> inductive -> constr array
-(** Given a record type, computes the legacy match-based projection of the
- projections.
-
- BEWARE: such terms are ill-typed, and should thus only be used in upper
- layers. The kernel will probably badly fail if presented with one of
- those. *)
-
(********************)
val type_of_inductive_knowing_conclusion :
diff --git a/pretyping/inferCumulativity.ml b/pretyping/inferCumulativity.ml
index b5a6ba6be5..bf8a38a353 100644
--- a/pretyping/inferCumulativity.ml
+++ b/pretyping/inferCumulativity.ml
@@ -41,33 +41,31 @@ let variance_pb cv_pb var =
| CONV, Covariant -> Invariant
| CUMUL, Covariant -> Covariant
-let infer_cumulative_ind_instance cv_pb cumi variances u =
+let infer_cumulative_ind_instance cv_pb mind_variance variances u =
Array.fold_left2 (fun variances varu u ->
match LMap.find u variances with
| exception Not_found -> variances
| varu' ->
LMap.set u (Variance.sup varu' (variance_pb cv_pb varu)) variances)
- variances (ACumulativityInfo.variance cumi) (Instance.to_array u)
+ variances mind_variance (Instance.to_array u)
let infer_inductive_instance cv_pb env variances ind nargs u =
let mind = Environ.lookup_mind (fst ind) env in
- match mind.mind_universes with
- | Monomorphic_ind _ -> assert (Instance.is_empty u); variances
- | Polymorphic_ind _ -> infer_generic_instance_eq variances u
- | Cumulative_ind cumi ->
+ match mind.mind_variance with
+ | None -> infer_generic_instance_eq variances u
+ | Some mind_variance ->
if not (Int.equal (inductive_cumulativity_arguments (mind,snd ind)) nargs)
then infer_generic_instance_eq variances u
- else infer_cumulative_ind_instance cv_pb cumi variances u
+ else infer_cumulative_ind_instance cv_pb mind_variance variances u
let infer_constructor_instance_eq env variances ((mi,ind),ctor) nargs u =
let mind = Environ.lookup_mind mi env in
- match mind.mind_universes with
- | Monomorphic_ind _ -> assert (Instance.is_empty u); variances
- | Polymorphic_ind _ -> infer_generic_instance_eq variances u
- | Cumulative_ind cumi ->
+ match mind.mind_variance with
+ | None -> infer_generic_instance_eq variances u
+ | Some _ ->
if not (Int.equal (constructor_cumulativity_arguments (mind,ind,ctor)) nargs)
then infer_generic_instance_eq variances u
- else infer_cumulative_ind_instance CONV cumi variances u
+ else variances (* constructors are convertible at common supertype *)
let infer_sort cv_pb variances s =
match cv_pb with
@@ -189,12 +187,14 @@ let infer_inductive env mie =
let { mind_entry_params = params;
mind_entry_inds = entries; } = mie
in
- let univs =
- match mie.mind_entry_universes with
- | Monomorphic_ind_entry _
- | Polymorphic_ind_entry _ as univs -> univs
- | Cumulative_ind_entry (nas, cumi) ->
- let uctx = CumulativityInfo.univ_context cumi in
+ let variances =
+ match mie.mind_entry_variance with
+ | None -> None
+ | Some _ ->
+ let uctx = match mie.mind_entry_universes with
+ | Monomorphic_entry _ -> assert false
+ | Polymorphic_entry (_,uctx) -> uctx
+ in
let uarray = Instance.to_array @@ UContext.instance uctx in
let env = Environ.push_context uctx env in
let variances =
@@ -212,6 +212,10 @@ let infer_inductive env mie =
entries
in
let variances = Array.map (fun u -> LMap.find u variances) uarray in
- Cumulative_ind_entry (nas, CumulativityInfo.make (uctx, variances))
+ Some variances
in
- { mie with mind_entry_universes = univs }
+ { mie with mind_entry_variance = variances }
+
+let dummy_variance = let open Entries in function
+ | Monomorphic_entry _ -> assert false
+ | Polymorphic_entry (_,uctx) -> Array.make (UContext.size uctx) Variance.Irrelevant
diff --git a/pretyping/inferCumulativity.mli b/pretyping/inferCumulativity.mli
index a0c8d339ac..6e5bf30f6b 100644
--- a/pretyping/inferCumulativity.mli
+++ b/pretyping/inferCumulativity.mli
@@ -10,3 +10,5 @@
val infer_inductive : Environ.env -> Entries.mutual_inductive_entry ->
Entries.mutual_inductive_entry
+
+val dummy_variance : Entries.universes_entry -> Univ.Variance.t array
diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml
index b7090e69da..77ae09ee6f 100644
--- a/pretyping/nativenorm.ml
+++ b/pretyping/nativenorm.ml
@@ -107,7 +107,8 @@ let find_rectype_a env c =
(* Instantiate inductives and parameters in constructor type *)
-let type_constructor mind mib u typ params =
+let type_constructor mind mib u (ctx, typ) params =
+ let typ = it_mkProd_or_LetIn typ ctx in
let s = ind_subst mind mib u in
let ctyp = substl s typ in
let nparams = Array.length params in
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 46e463512d..a92b245b91 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -103,6 +103,12 @@ let search_guard ?loc env possible_indexes fixdefs =
user_err ?loc ~hdr:"search_guard" (Pp.str errmsg)
with Found indexes -> indexes)
+let esearch_guard ?loc env sigma indexes fix =
+ let fix = nf_fix sigma fix in
+ try search_guard ?loc env indexes fix
+ with TypeError (env,err) ->
+ raise (PretypeError (env,sigma,TypingError (map_ptype_error of_constr err)))
+
(* To force universe name declaration before use *)
let is_strict_universe_declarations =
@@ -597,11 +603,8 @@ let rec pretype ~program_mode k0 resolve_tc (tycon : type_constraint) (env : Glo
vn)
in
let fixdecls = (names,ftys,fdefs) in
- let indexes =
- search_guard
- ?loc !!env possible_indexes (nf_fix sigma fixdecls)
- in
- make_judge (mkFix ((indexes,i),fixdecls)) ftys.(i)
+ let indexes = esearch_guard ?loc !!env sigma possible_indexes fixdecls in
+ make_judge (mkFix ((indexes,i),fixdecls)) ftys.(i)
| GCoFix i ->
let fixdecls = (names,ftys,fdefs) in
let cofix = (i, fixdecls) in
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index e8d935fcbb..2e50e1ab3f 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -244,10 +244,10 @@ let judge_of_type u =
uj_type = EConstr.mkType uu }
let judge_of_relative env v =
- Termops.on_judgment EConstr.of_constr (judge_of_relative env v)
+ Environ.on_judgment EConstr.of_constr (judge_of_relative env v)
let judge_of_variable env id =
- Termops.on_judgment EConstr.of_constr (judge_of_variable env id)
+ Environ.on_judgment EConstr.of_constr (judge_of_variable env id)
let judge_of_projection env sigma p cj =
let pty = lookup_projection p env in
@@ -307,7 +307,7 @@ let type_of_constructor env sigma ((ind,_ as ctor),u) =
sigma, (EConstr.of_constr (rename_type ty (Names.GlobRef.ConstructRef ctor)))
let judge_of_int env v =
- Termops.on_judgment EConstr.of_constr (judge_of_int env v)
+ Environ.on_judgment EConstr.of_constr (judge_of_int env v)
(* cstr must be in n.f. w.r.t. evars and execute returns a judgement
where both the term and type are in n.f. *)
diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml
index 083661a64b..ff528bd2cf 100644
--- a/pretyping/vnorm.ml
+++ b/pretyping/vnorm.ml
@@ -61,7 +61,8 @@ let find_rectype_a env c =
(* Instantiate inductives and parameters in constructor type *)
-let type_constructor mind mib u typ params =
+let type_constructor mind mib u (ctx, typ) params =
+ let typ = it_mkProd_or_LetIn typ ctx in
let s = ind_subst mind mib u in
let ctyp = substl s typ in
let ctyp = subst_instance_constr u ctyp in
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-03 01:20:25 +0000