aboutsummaryrefslogtreecommitdiff
path: root/pretyping
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping')
-rw-r--r--pretyping/coercion.ml4
-rw-r--r--pretyping/constr_matching.ml4
-rw-r--r--pretyping/detyping.ml4
-rw-r--r--pretyping/evarsolve.ml2
-rw-r--r--pretyping/glob_ops.ml4
-rw-r--r--pretyping/indrec.ml9
-rw-r--r--pretyping/inductiveops.ml24
-rw-r--r--pretyping/inductiveops.mli12
-rw-r--r--pretyping/nativenorm.ml41
-rw-r--r--pretyping/patternops.ml4
-rw-r--r--pretyping/retyping.ml13
-rw-r--r--pretyping/typeclasses.ml4
-rw-r--r--pretyping/typeclasses.mli4
-rw-r--r--pretyping/typing.ml13
-rw-r--r--pretyping/vnorm.ml39
15 files changed, 82 insertions, 99 deletions
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index bf9e37aa74..5c4cbefad8 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -209,8 +209,8 @@ and coerce ?loc env evdref (x : EConstr.constr) (y : EConstr.constr)
match (EConstr.kind !evdref x, EConstr.kind !evdref y) with
| Sort s, Sort s' ->
(match ESorts.kind !evdref s, ESorts.kind !evdref s' with
- | Prop x, Prop y when x == y -> None
- | Prop _, Type _ -> None
+ | Prop, Prop | Set, Set -> None
+ | (Prop | Set), Type _ -> None
| Type x, Type y when Univ.Universe.equal x y -> None (* false *)
| _ -> subco ())
| Prod (name, a, b), Prod (name', a', b') ->
diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml
index 2bc603a902..d7118efd7a 100644
--- a/pretyping/constr_matching.ml
+++ b/pretyping/constr_matching.ml
@@ -281,8 +281,8 @@ let matches_core env sigma allow_bound_rels
let open Glob_term in
begin match ps, ESorts.kind sigma s with
- | GProp, Prop Null -> subst
- | GSet, Prop Pos -> subst
+ | GProp, Prop -> subst
+ | GSet, Set -> subst
| GType _, Type _ -> subst
| _ -> raise PatternMatchingFailure
end
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 23a985dc3e..d0de2f8c0c 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -597,8 +597,8 @@ let detype_universe sigma u =
Univ.Universe.map fn u
let detype_sort sigma = function
- | Prop Null -> GProp
- | Prop Pos -> GSet
+ | Prop -> GProp
+ | Set -> GSet
| Type u ->
GType
(if !print_universes
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index 8afb9b9421..3f5d186d4e 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -69,7 +69,7 @@ let refresh_universes ?(status=univ_rigid) ?(onlyalg=false) ?(refreshset=false)
if onlyalg && alg then
(evdref := Evd.make_flexible_variable !evdref ~algebraic:false l; t)
else t))
- | Prop Pos when refreshset && not direction ->
+ | Set when refreshset && not direction ->
(* Cannot make a universe "lower" than "Set",
only refreshing when we want higher universes. *)
refresh_sort status ~direction s
diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml
index ba193da60d..4dfa789ba5 100644
--- a/pretyping/glob_ops.ml
+++ b/pretyping/glob_ops.ml
@@ -112,7 +112,7 @@ let fix_kind_eq f k1 k2 = match k1, k2 with
let eq (i1, o1) (i2, o2) =
Option.equal Int.equal i1 i2 && fix_recursion_order_eq f o1 o2
in
- Int.equal i1 i2 && Array.equal eq a1 a1
+ Int.equal i1 i2 && Array.equal eq a1 a2
| GCoFix i1, GCoFix i2 -> Int.equal i1 i2
| (GFix _ | GCoFix _), _ -> false
@@ -452,7 +452,7 @@ let rec rename_glob_vars l c = force @@ DAst.map_with_loc (fun ?loc -> function
else r
| GProd (na,bk,t,c) ->
let na',l' = update_subst na l in
- GProd (na,bk,rename_glob_vars l t,rename_glob_vars l' c)
+ GProd (na',bk,rename_glob_vars l t,rename_glob_vars l' c)
| GLambda (na,bk,t,c) ->
let na',l' = update_subst na l in
GLambda (na',bk,rename_glob_vars l t,rename_glob_vars l' c)
diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml
index 4ab932723e..551cc67b60 100644
--- a/pretyping/indrec.ml
+++ b/pretyping/indrec.ml
@@ -86,7 +86,7 @@ let mis_make_case_com dep env sigma (ind, u as pind) (mib,mip as specif) kind =
if not (Sorts.List.mem kind (elim_sorts specif)) then
raise
(RecursionSchemeError
- (NotAllowedCaseAnalysis (false, fst (UnivGen.fresh_sort_in_family env kind), pind)))
+ (NotAllowedCaseAnalysis (false, fst (UnivGen.fresh_sort_in_family kind), pind)))
in
let ndepar = mip.mind_nrealdecls + 1 in
@@ -136,7 +136,7 @@ let mis_make_case_com dep env sigma (ind, u as pind) (mib,mip as specif) kind =
mkLambda_string "f" t
(add_branch (push_rel (LocalAssum (Anonymous, t)) env) (k+1))
in
- let (sigma, s) = Evd.fresh_sort_in_family ~rigid:Evd.univ_flexible_alg env sigma kind in
+ let (sigma, s) = Evd.fresh_sort_in_family ~rigid:Evd.univ_flexible_alg sigma kind in
let typP = make_arity env' sigma dep indf s in
let typP = EConstr.Unsafe.to_constr typP in
let c =
@@ -455,7 +455,7 @@ let mis_make_indrec env sigma ?(force_mutual=false) listdepkind mib u =
| ((indi,u),_,_,dep,kinds)::rest ->
let indf = make_ind_family ((indi,u), Context.Rel.to_extended_list mkRel i lnamesparrec) in
let s =
- Evarutil.evd_comb1 (Evd.fresh_sort_in_family ~rigid:Evd.univ_flexible_alg env)
+ Evarutil.evd_comb1 (Evd.fresh_sort_in_family ~rigid:Evd.univ_flexible_alg)
evdref kinds
in
let typP = make_arity env !evdref dep indf s in
@@ -550,8 +550,7 @@ let check_arities env listdepkind =
let kelim = elim_sorts (mibi,mipi) in
if not (Sorts.List.mem kind kelim) then raise
(RecursionSchemeError
- (NotAllowedCaseAnalysis (true, fst (UnivGen.fresh_sort_in_family env
- kind),(mind,u))))
+ (NotAllowedCaseAnalysis (true, fst (UnivGen.fresh_sort_in_family kind),(mind,u))))
else if Int.List.mem ni ln then raise
(RecursionSchemeError (NotMutualInScheme (mind,mind)))
else ni::ln)
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index d599afe699..5760733442 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -303,7 +303,7 @@ type constructor_summary = {
cs_cstr : pconstructor;
cs_params : constr list;
cs_nargs : int;
- cs_args : Context.Rel.t;
+ cs_args : Constr.rel_context;
cs_concl_realargs : constr array
}
@@ -465,22 +465,21 @@ 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 indu = match mib.mind_universes with
- | Monomorphic_ind _ -> mkInd ind
- | Polymorphic_ind ctx -> mkIndU (ind, make_abstract_instance ctx)
- | Cumulative_ind ctx ->
- mkIndU (ind, make_abstract_instance (ACumulativityInfo.univ_context ctx))
+ 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 x = match mib.mind_record with
| NotRecord | FakeRecord ->
anomaly Pp.(str "Trying to build primitive projections for a non-primitive record")
| PrimRecord info-> Name (pi1 (info.(i)))
in
- (** FIXME: handle mutual records *)
- let pkt = mib.mind_packets.(0) in
- let { mind_consnrealargs; mind_consnrealdecls } = pkt in
+ let pkt = mib.mind_packets.(i) in
let { mind_nparams = nparamargs; mind_params_ctxt = params } = mib in
- let rctx, _ = decompose_prod_assum (subst1 indu pkt.mind_nf_lc.(0)) 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, paramslet = List.chop pkt.mind_consnrealdecls.(0) rctx in
let mp, dp, l = MutInd.repr3 kn in
(** We build a substitution smashing the lets in the record parameters so
@@ -489,6 +488,7 @@ let compute_projections env (kn, i as ind) =
let indty =
(* [ty] = [Ind inst] is typed in context [params] *)
let inst = Context.Rel.to_extended_vect mkRel 0 paramslet in
+ let indu = mkIndU (ind, u) in
let ty = mkApp (indu, inst) in
(* [Ind inst] is typed in context [params-wo-let] *)
ty
@@ -498,8 +498,8 @@ let compute_projections env (kn, i as ind) =
{ ind_tags = []; cstr_tags = [|Context.Rel.to_tags ctx|]; style = LetStyle } in
{ ci_ind = ind;
ci_npar = nparamargs;
- ci_cstr_ndecls = mind_consnrealdecls;
- ci_cstr_nargs = mind_consnrealargs;
+ ci_cstr_ndecls = pkt.mind_consnrealdecls;
+ ci_cstr_nargs = pkt.mind_consnrealargs;
ci_pp_info = print_info }
in
let len = List.length ctx in
diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli
index aa53f7e67c..8eaef24c48 100644
--- a/pretyping/inductiveops.mli
+++ b/pretyping/inductiveops.mli
@@ -93,12 +93,12 @@ val inductive_nparamdecls : inductive -> int
val inductive_nparamdecls_env : env -> inductive -> int
(** @return params context *)
-val inductive_paramdecls : pinductive -> Context.Rel.t
-val inductive_paramdecls_env : env -> pinductive -> Context.Rel.t
+val inductive_paramdecls : pinductive -> Constr.rel_context
+val inductive_paramdecls_env : env -> pinductive -> Constr.rel_context
(** @return full arity context, hence with letin *)
-val inductive_alldecls : pinductive -> Context.Rel.t
-val inductive_alldecls_env : env -> pinductive -> Context.Rel.t
+val inductive_alldecls : pinductive -> Constr.rel_context
+val inductive_alldecls_env : env -> pinductive -> Constr.rel_context
(** {7 Extract information from a constructor name} *)
@@ -141,7 +141,7 @@ type constructor_summary = {
cs_cstr : pconstructor; (* internal name of the constructor plus universes *)
cs_params : constr list; (* parameters of the constructor in current ctx *)
cs_nargs : int; (* length of arguments signature (letin included) *)
- cs_args : Context.Rel.t; (* signature of the arguments (letin included) *)
+ cs_args : Constr.rel_context; (* signature of the arguments (letin included) *)
cs_concl_realargs : constr array; (* actual realargs in the concl of cstr *)
}
val lift_constructor : int -> constructor_summary -> constructor_summary
@@ -154,7 +154,7 @@ val get_projections : env -> inductive_family -> Constant.t array option
(** [get_arity] returns the arity of the inductive family instantiated
with the parameters; if recursively non-uniform parameters are not
part of the inductive family, they appears in the arity *)
-val get_arity : env -> inductive_family -> Context.Rel.t * Sorts.family
+val get_arity : env -> inductive_family -> Constr.rel_context * Sorts.family
val build_dependent_constructor : constructor_summary -> constr
val build_dependent_inductive : env -> inductive_family -> constr
diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml
index 7319846fb3..21c2022057 100644
--- a/pretyping/nativenorm.ml
+++ b/pretyping/nativenorm.ml
@@ -123,7 +123,7 @@ let construct_of_constr_notnative const env tag (mind, _ as ind) u allargs =
try
if const then
let ctyp = type_constructor mind mib u (mip.mind_nf_lc.(0)) params in
- retroknowledge Retroknowledge.get_vm_decompile_constant_info env (mkInd ind) tag, ctyp
+ Retroknowledge.get_vm_decompile_constant_info env.retroknowledge (mkInd ind) tag, ctyp
else
raise Not_found
with Not_found ->
@@ -144,7 +144,7 @@ let construct_of_constr_const env tag typ =
let construct_of_constr_block = construct_of_constr false
-let build_branches_type env sigma (mind,_ as _ind) mib mip u params dep p =
+let build_branches_type env sigma (mind,_ as _ind) mib mip u params p =
let rtbl = mip.mind_reloc_tbl in
(* [build_one_branch i cty] construit le type de la ieme branche (commence
a 0) et les lambda correspondant aux realargs *)
@@ -161,20 +161,17 @@ let build_branches_type env sigma (mind,_ as _ind) mib mip u params dep p =
let codom =
let ndecl = List.length decl in
let papp = mkApp(lift ndecl p,crealargs) in
- if dep then
- let cstr = ith_constructor_of_inductive (fst ind) (i+1) in
- let relargs = Array.init carity (fun i -> mkRel (carity-i)) in
- let params = Array.map (lift ndecl) params in
- let dep_cstr = mkApp(mkApp(mkConstructU (cstr,snd ind),params),relargs) in
- mkApp(papp,[|dep_cstr|])
- else papp
+ let cstr = ith_constructor_of_inductive (fst ind) (i+1) in
+ let relargs = Array.init carity (fun i -> mkRel (carity-i)) in
+ let params = Array.map (lift ndecl) params in
+ let dep_cstr = mkApp(mkApp(mkConstructU (cstr,snd ind),params),relargs) in
+ mkApp(papp,[|dep_cstr|])
in
decl, decl_with_letin, codom
in Array.mapi build_one_branch mip.mind_nf_lc
-let build_case_type dep p realargs c =
- if dep then mkApp(mkApp(p, realargs), [|c|])
- else mkApp(p, realargs)
+let build_case_type p realargs c =
+ mkApp(mkApp(p, realargs), [|c|])
(* normalisation of values *)
@@ -317,9 +314,9 @@ and nf_atom_type env sigma atom =
let pT =
hnf_prod_applist_assum env nparamdecls
(Inductiveops.type_of_inductive env ind) (Array.to_list params) in
- let dep, p = nf_predicate env sigma ind mip params p pT in
+ let p = nf_predicate env sigma ind mip params p pT in
(* Calcul du type des branches *)
- let btypes = build_branches_type env sigma (fst ind) mib mip u params dep p in
+ let btypes = build_branches_type env sigma (fst ind) mib mip u params p in
(* calcul des branches *)
let bsw = branch_of_switch (nb_rel env) ans bs in
let mkbranch i v =
@@ -328,7 +325,7 @@ and nf_atom_type env sigma atom =
Termops.it_mkLambda_or_LetIn_from_no_LetIn b decl_with_letin
in
let branchs = Array.mapi mkbranch bsw in
- let tcase = build_case_type dep p realargs a in
+ let tcase = build_case_type p realargs a in
let ci = ans.asw_ci in
mkCase(ci, p, a, branchs), tcase
| Afix(tt,ft,rp,s) ->
@@ -375,18 +372,18 @@ and nf_atom_type env sigma atom =
and nf_predicate env sigma ind mip params v pT =
match kind (whd_allnolet env pT) with
| LetIn (name,b,t,pT) ->
- let dep,body =
+ let body =
nf_predicate (push_rel (LocalDef (name,b,t)) env) sigma ind mip params v pT in
- dep, mkLetIn (name,b,t,body)
+ mkLetIn (name,b,t,body)
| Prod (name,dom,codom) -> begin
match kind_of_value v with
| Vfun f ->
let k = nb_rel env in
let vb = f (mk_rel_accu k) in
- let dep,body =
+ let body =
nf_predicate (push_rel (LocalAssum (name,dom)) env) sigma ind mip params vb codom in
- dep, mkLambda(name,dom,body)
- | _ -> false, nf_type env sigma v
+ mkLambda(name,dom,body)
+ | _ -> nf_type env sigma v
end
| _ ->
match kind_of_value v with
@@ -399,8 +396,8 @@ and nf_predicate env sigma ind mip params v pT =
let params = if Int.equal n 0 then params else Array.map (lift n) params in
let dom = mkApp(mkIndU ind,Array.append params rargs) in
let body = nf_type (push_rel (LocalAssum (name,dom)) env) sigma vb in
- true, mkLambda(name,dom,body)
- | _ -> false, nf_type env sigma v
+ mkLambda(name,dom,body)
+ | _ -> nf_type env sigma v
and nf_evar env sigma evk ty args =
let evi = try Evd.find sigma evk with Not_found -> assert false in
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index 622a8e982e..685aa400b8 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -150,8 +150,8 @@ let pattern_of_constr env sigma t =
| Rel n -> PRel n
| Meta n -> PMeta (Some (Id.of_string ("META" ^ string_of_int n)))
| Var id -> PVar id
- | Sort (Prop Null) -> PSort GProp
- | Sort (Prop Pos) -> PSort GSet
+ | Sort Prop -> PSort GProp
+ | Sort Set -> PSort GSet
| Sort (Type _) -> PSort (GType [])
| Cast (c,_,_) -> pattern_of_constr env c
| LetIn (na,c,t,b) -> PLetIn (na,pattern_of_constr env c,Some (pattern_of_constr env t),
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index 746a68b217..7e43c5e41d 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -149,18 +149,13 @@ let retype ?(polyprop=true) sigma =
| Cast (c,_, s) when isSort sigma s -> destSort sigma s
| Sort s ->
begin match ESorts.kind sigma s with
- | Prop _ -> Sorts.type1
+ | Prop | Set -> Sorts.type1
| Type u -> Type (Univ.super u)
end
| Prod (name,t,c2) ->
- (match (sort_of env t, sort_of (push_rel (LocalAssum (name,t)) env) c2) with
- | _, (Prop Null as s) -> s
- | Prop _, (Prop Pos as s) -> s
- | Type _, (Prop Pos as s) when is_impredicative_set env -> s
- | Type u1, Prop Pos -> Type (Univ.sup u1 Univ.type0_univ)
- | Prop Pos, (Type u2) -> Type (Univ.sup Univ.type0_univ u2)
- | Prop Null, (Type _ as s) -> s
- | Type u1, Type u2 -> Type (Univ.sup u1 u2))
+ let dom = sort_of env t in
+ let rang = sort_of (push_rel (LocalAssum (name,t)) env) c2 in
+ Typeops.sort_of_product env dom rang
| App(f,args) when is_template_polymorphic env sigma f ->
let t = type_of_global_reference_knowing_parameters env f args in
sort_of_atomic_type env sigma t args
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index d3aa7ac643..efb3c339ac 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -74,10 +74,10 @@ type typeclass = {
cl_impl : GlobRef.t;
(* Context in which the definitions are typed. Includes both typeclass parameters and superclasses. *)
- cl_context : GlobRef.t option list * Context.Rel.t;
+ cl_context : GlobRef.t option list * Constr.rel_context;
(* Context of definitions and properties on defs, will not be shared *)
- cl_props : Context.Rel.t;
+ cl_props : Constr.rel_context;
(* The method implementaions as projections. *)
cl_projs : (Name.t * (direction * hint_info) option
diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli
index e4a56960cf..80c6d82397 100644
--- a/pretyping/typeclasses.mli
+++ b/pretyping/typeclasses.mli
@@ -35,10 +35,10 @@ type typeclass = {
(** Context in which the definitions are typed. Includes both typeclass parameters and superclasses.
The global reference gives a direct link to the class itself. *)
- cl_context : GlobRef.t option list * Context.Rel.t;
+ cl_context : GlobRef.t option list * Constr.rel_context;
(** Context of definitions and properties on defs, will not be shared *)
- cl_props : Context.Rel.t;
+ cl_props : Constr.rel_context;
(** The methods implementations of the typeclass as projections.
Some may be undefinable due to sorting restrictions or simply undefined if
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index cf34ac0164..ca2702d741 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -138,7 +138,7 @@ let is_correct_arity env sigma c pj ind specif params =
then error ()
else sigma
| Evar (ev,_), [] ->
- let sigma, s = Evd.fresh_sort_in_family env sigma (max_sort allowed_sorts) in
+ let sigma, s = Evd.fresh_sort_in_family sigma (max_sort allowed_sorts) in
let sigma = Evd.define ev (mkSort s) sigma in
sigma
| _, (LocalDef _ as d)::ar' ->
@@ -241,10 +241,6 @@ let judge_of_set =
{ uj_val = EConstr.mkSet;
uj_type = EConstr.mkSort Sorts.type1 }
-let judge_of_prop_contents = function
- | Null -> judge_of_prop
- | Pos -> judge_of_set
-
let judge_of_type u =
let uu = Univ.Universe.super u in
{ uj_val = EConstr.mkType u;
@@ -333,10 +329,9 @@ let rec execute env sigma cstr =
| Sort s ->
begin match ESorts.kind sigma s with
- | Prop c ->
- sigma, judge_of_prop_contents c
- | Type u ->
- sigma, judge_of_type u
+ | Prop -> sigma, judge_of_prop
+ | Set -> sigma, judge_of_set
+ | Type u -> sigma, judge_of_type u
end
| Proj (p, c) ->
diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml
index 14c9f49b12..440076c165 100644
--- a/pretyping/vnorm.ml
+++ b/pretyping/vnorm.ml
@@ -79,7 +79,7 @@ let construct_of_constr const env tag typ =
(* spiwack : here be a branch for specific decompilation handled by retroknowledge *)
try
if const then
- ((retroknowledge Retroknowledge.get_vm_decompile_constant_info env (mkIndU indu) tag),
+ ((Retroknowledge.get_vm_decompile_constant_info env.retroknowledge (mkIndU indu) tag),
typ) (*spiwack: this may need to be changed in case there are parameters in the
type which may cause a constant value to have an arity.
(type_constructor seems to be all about parameters actually)
@@ -103,7 +103,7 @@ let construct_of_constr_block = construct_of_constr false
let type_of_ind env (ind, u) =
type_of_inductive env (Inductive.lookup_mind_specif env ind, u)
-let build_branches_type env sigma (mind,_ as _ind) mib mip u params dep p =
+let build_branches_type env sigma (mind,_ as _ind) mib mip u params p =
let rtbl = mip.mind_reloc_tbl in
(* [build_one_branch i cty] construit le type de la ieme branche (commence
a 0) et les lambda correspondant aux realargs *)
@@ -120,20 +120,17 @@ let build_branches_type env sigma (mind,_ as _ind) mib mip u params dep p =
let codom =
let ndecl = List.length decl in
let papp = mkApp(lift ndecl p,crealargs) in
- if dep then
- let cstr = ith_constructor_of_inductive ind (i+1) in
- let relargs = Array.init carity (fun i -> mkRel (carity-i)) in
- let params = Array.map (lift ndecl) params in
- let dep_cstr = mkApp(mkApp(mkConstructU (cstr,u),params),relargs) in
- mkApp(papp,[|dep_cstr|])
- else papp
+ let cstr = ith_constructor_of_inductive ind (i+1) in
+ let relargs = Array.init carity (fun i -> mkRel (carity-i)) in
+ let params = Array.map (lift ndecl) params in
+ let dep_cstr = mkApp(mkApp(mkConstructU (cstr,u),params),relargs) in
+ mkApp(papp,[|dep_cstr|])
in
decl, decl_with_letin, codom
in Array.mapi build_one_branch mip.mind_nf_lc
-let build_case_type dep p realargs c =
- if dep then mkApp(mkApp(p, realargs), [|c|])
- else mkApp(p, realargs)
+let build_case_type p realargs c =
+ mkApp(mkApp(p, realargs), [|c|])
(* La fonction de normalisation *)
@@ -266,9 +263,9 @@ and nf_stk ?from:(from=0) env sigma c t stk =
let nparamdecls = Context.Rel.length (Inductive.inductive_paramdecls (mib,u)) in
let pT =
hnf_prod_applist_assum env nparamdecls (type_of_ind env (ind,u)) (Array.to_list params) in
- let dep, p = nf_predicate env sigma (ind,u) mip params (type_of_switch sw) pT in
+ let p = nf_predicate env sigma (ind,u) mip params (type_of_switch sw) pT in
(* Calcul du type des branches *)
- let btypes = build_branches_type env sigma ind mib mip u params dep p in
+ let btypes = build_branches_type env sigma ind mib mip u params p in
(* calcul des branches *)
let bsw = branch_of_switch (nb_rel env) sw in
let mkbranch i (n,v) =
@@ -277,7 +274,7 @@ and nf_stk ?from:(from=0) env sigma c t stk =
Termops.it_mkLambda_or_LetIn_from_no_LetIn b decl_with_letin
in
let branchs = Array.mapi mkbranch bsw in
- let tcase = build_case_type dep p realargs c in
+ let tcase = build_case_type p realargs c in
let ci = sw.sw_annot.Cbytecodes.ci in
nf_stk env sigma (mkCase(ci, p, c, branchs)) tcase stk
| Zproj p :: stk ->
@@ -289,17 +286,17 @@ and nf_stk ?from:(from=0) env sigma c t stk =
and nf_predicate env sigma ind mip params v pT =
match kind (whd_allnolet env pT) with
| LetIn (name,b,t,pT) ->
- let dep,body =
+ let body =
nf_predicate (push_rel (LocalDef (name,b,t)) env) sigma ind mip params v pT in
- dep, mkLetIn (name,b,t,body)
+ mkLetIn (name,b,t,body)
| Prod (name,dom,codom) -> begin
match whd_val v with
| Vfun f ->
let k = nb_rel env in
let vb = reduce_fun k f in
- let dep,body =
+ let body =
nf_predicate (push_rel (LocalAssum (name,dom)) env) sigma ind mip params vb codom in
- dep, mkLambda(name,dom,body)
+ mkLambda(name,dom,body)
| _ -> assert false
end
| _ ->
@@ -313,8 +310,8 @@ and nf_predicate env sigma ind mip params v pT =
let params = if Int.equal n 0 then params else Array.map (lift n) params in
let dom = mkApp(mkIndU ind,Array.append params rargs) in
let body = nf_vtype (push_rel (LocalAssum (name,dom)) env) sigma vb in
- true, mkLambda(name,dom,body)
- | _ -> false, nf_val env sigma v crazy_type
+ mkLambda(name,dom,body)
+ | _ -> nf_val env sigma v crazy_type
and nf_args env sigma vargs ?from:(f=0) t =
let t = ref t in
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-03 14:57:52 +0000