aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--kernel/environ.ml2
-rw-r--r--kernel/inductive.ml12
-rw-r--r--kernel/inductive.mli6
-rw-r--r--kernel/reduction.mli2
-rw-r--r--kernel/sign.ml13
-rw-r--r--kernel/sign.mli12
-rw-r--r--kernel/type_errors.ml2
-rw-r--r--kernel/type_errors.mli4
-rw-r--r--kernel/typeops.ml6
9 files changed, 29 insertions, 30 deletions
diff --git a/kernel/environ.ml b/kernel/environ.ml
index ff280fa15..e03d489c7 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -328,7 +328,7 @@ let make_judge v tj =
uj_type = tj }
let j_val j = j.uj_val
-let j_type j = body_of_type j.uj_type
+let j_type j = j.uj_type
type unsafe_type_judgment = {
utj_val : constr;
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 4cfc1d2af..d7181299e 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -73,12 +73,12 @@ let lookup_mind_instance (sp,tyi) env =
let ind_subst mispec =
let ntypes = mispec.mis_mib.mind_ntypes in
let make_Ik k = mkInd (mispec.mis_sp,ntypes-k-1) in
- (list_tabulate make_Ik ntypes)
+ list_tabulate make_Ik ntypes
(* Instantiate both section variables and inductives *)
-let constructor_instantiate mispec =
+let constructor_instantiate mispec c =
let s = ind_subst mispec in
- substl s
+ type_app (substl s) c
(* Instantiate the parameters of the inductive type *)
(* TODO: verify the arg of LetIn correspond to the value in the
@@ -96,7 +96,7 @@ let instantiate_params t args sign =
sign
(args,[],t) in
if rem_args <> [] then fail();
- substl subs ty
+ type_app (substl subs) ty
let full_inductive_instantiate (mispec,params) t =
instantiate_params t params mispec.mis_mip.mind_params_ctxt
@@ -496,7 +496,7 @@ let rec check_subterm_rec_meta env vectn k def =
| Lambda (x,a,b) ->
if noccur_with_meta n nfi a then
let env' = push_rel (x, None, a) env in
- if n = k+1 then (env', lift 1 a, b)
+ if n = k+1 then (env', type_app (lift 1) a, b)
else check_occur env' (n+1) b
else
anomaly "check_subterm_rec_meta: Bad occurrence of recursive call"
@@ -696,7 +696,7 @@ let anomaly_ill_typed () =
let check_guard_rec_meta env nbfix def deftype =
let rec codomain_is_coind env c =
- let b = whd_betadeltaiota env (strip_outer_cast c) in
+ let b = whd_betadeltaiota env c in
match kind_of_term b with
| Prod (x,a,b) ->
codomain_is_coind (push_rel (x, None, a) env) b
diff --git a/kernel/inductive.mli b/kernel/inductive.mli
index d9add1e6f..7e08a31c0 100644
--- a/kernel/inductive.mli
+++ b/kernel/inductive.mli
@@ -26,9 +26,9 @@ exception Induc
only a coinductive type.
They raise [Induc] if not convertible to a recursive type. *)
-val find_rectype : env -> constr -> inductive * constr list
-val find_inductive : env -> constr -> inductive * constr list
-val find_coinductive : env -> constr -> inductive * constr list
+val find_rectype : env -> types -> inductive * constr list
+val find_inductive : env -> types -> inductive * constr list
+val find_coinductive : env -> types -> inductive * constr list
(*s Fetching information in the environment about an inductive type.
Raises Induc if the inductive type is not found. *)
diff --git a/kernel/reduction.mli b/kernel/reduction.mli
index 625833547..9ac3d8042 100644
--- a/kernel/reduction.mli
+++ b/kernel/reduction.mli
@@ -33,7 +33,7 @@ exception NotConvertible
exception NotConvertibleVect of int
type 'a conversion_function = env -> 'a -> 'a -> Univ.constraints
-val conv : constr conversion_function
+val conv : types conversion_function
val conv_leq : types conversion_function
val conv_leq_vecti : types array conversion_function
diff --git a/kernel/sign.ml b/kernel/sign.ml
index 61b23ec26..05038840d 100644
--- a/kernel/sign.ml
+++ b/kernel/sign.ml
@@ -75,15 +75,14 @@ let push_named_to_rel_context hyps ctxt =
let rec push = function
| (id,b,t) :: l ->
let s, hyps = push l in
- let d = (Name id, option_app (subst_vars s) b, subst_vars s t) in
+ let d = (Name id, option_app (subst_vars s) b, type_app (subst_vars s) t) in
id::s, d::hyps
| [] -> [],[] in
let s, hyps = push hyps in
let rec subst = function
- | (na,b,t) :: l ->
+ | d :: l ->
let n, ctxt = subst l in
- let d = (na, option_app (substn_vars n s) b, substn_vars n s t) in
- (n+1), d::ctxt
+ (n+1), (map_rel_declaration (substn_vars n s) d)::ctxt
| [] -> 1, hyps in
snd (subst ctxt)
@@ -116,7 +115,7 @@ let destArity =
| Sort s -> l,s
| _ -> anomaly "destArity: not an arity"
in
- prodec_rec []
+ prodec_rec []
let rec isArity c =
match kind_of_term c with
@@ -156,14 +155,14 @@ let decompose_prod_n_assum n =
if n < 0 then
error "decompose_prod_n_assum: integer parameter must be positive";
let rec prodec_rec l n c =
- if n=0 then l,c
+ if n=0 then l,c
else match kind_of_term c with
| Prod (x,t,c) -> prodec_rec (add_rel_decl (x,None,t) l) (n-1) c
| LetIn (x,b,t,c) -> prodec_rec (add_rel_decl (x,Some b,t) l) (n-1) c
| Cast (c,_) -> prodec_rec l n c
| c -> error "decompose_prod_n_assum: not enough assumptions"
in
- prodec_rec empty_rel_context n
+ prodec_rec empty_rel_context n
(* Given a positive integer n, transforms a lambda term [x1:T1]..[xn:Tn]T
into the pair ([(xn,Tn);...;(x1,T1)],T) *)
diff --git a/kernel/sign.mli b/kernel/sign.mli
index 61e97d9eb..fbc682e35 100644
--- a/kernel/sign.mli
+++ b/kernel/sign.mli
@@ -59,22 +59,22 @@ val fold_rel_context_reverse :
(*s Term constructors *)
val it_mkNamedLambda_or_LetIn : constr -> named_context -> constr
-val it_mkNamedProd_or_LetIn : constr -> named_context -> constr
+val it_mkNamedProd_or_LetIn : types -> named_context -> types
val it_mkLambda_or_LetIn : constr -> rel_context -> constr
-val it_mkProd_or_LetIn : constr -> rel_context -> constr
+val it_mkProd_or_LetIn : types -> rel_context -> types
(*s Term destructors *)
(* Destructs a term of the form $(x_1:T_1)..(x_n:T_n)s$ into the pair *)
type arity = rel_context * sorts
-val destArity : constr -> arity
-val isArity : constr -> bool
+val destArity : types -> arity
+val isArity : types -> bool
(* Transforms a product term $(x_1:T_1)..(x_n:T_n)T$ including letins
into the pair $([(x_n,T_n);...;(x_1,T_1)],T)$, where $T$ is not a
product nor a let. *)
-val decompose_prod_assum : constr -> rel_context * constr
+val decompose_prod_assum : types -> rel_context * types
(* Transforms a lambda term $[x_1:T_1]..[x_n:T_n]T$ including letins
into the pair $([(x_n,T_n);...;(x_1,T_1)],T)$, where $T$ is not a
@@ -84,7 +84,7 @@ val decompose_lam_assum : constr -> rel_context * constr
(* Given a positive integer n, transforms a product term
$(x_1:T_1)..(x_n:T_n)T$
into the pair $([(xn,Tn);...;(x1,T1)],T)$. *)
-val decompose_prod_n_assum : int -> constr -> rel_context * constr
+val decompose_prod_n_assum : int -> types -> rel_context * types
(* Given a positive integer $n$, transforms a lambda term
$[x_1:T_1]..[x_n:T_n]T$ into the pair $([(x_n,T_n);...;(x_1,T_1)],T)$ *)
diff --git a/kernel/type_errors.ml b/kernel/type_errors.ml
index b057ff839..f1eb32b5b 100644
--- a/kernel/type_errors.ml
+++ b/kernel/type_errors.ml
@@ -40,7 +40,7 @@ type type_error =
| NotAType of unsafe_judgment
| BadAssumption of unsafe_judgment
| ReferenceVariables of constr
- | ElimArity of inductive * constr list * constr * unsafe_judgment
+ | ElimArity of inductive * types list * constr * unsafe_judgment
* (constr * constr * string) option
| CaseNotInductive of unsafe_judgment
| WrongCaseInfo of inductive * case_info
diff --git a/kernel/type_errors.mli b/kernel/type_errors.mli
index 3ffb585c5..99b46877a 100644
--- a/kernel/type_errors.mli
+++ b/kernel/type_errors.mli
@@ -42,7 +42,7 @@ type type_error =
| NotAType of unsafe_judgment
| BadAssumption of unsafe_judgment
| ReferenceVariables of constr
- | ElimArity of inductive * constr list * constr * unsafe_judgment
+ | ElimArity of inductive * types list * constr * unsafe_judgment
* (constr * constr * string) option
| CaseNotInductive of unsafe_judgment
| WrongCaseInfo of inductive * case_info
@@ -70,7 +70,7 @@ val error_assumption : env -> unsafe_judgment -> 'a
val error_reference_variables : env -> constr -> 'a
val error_elim_arity :
- env -> inductive -> constr list -> constr
+ env -> inductive -> types list -> constr
-> unsafe_judgment -> (constr * constr * string) option -> 'a
val error_case_not_inductive : env -> unsafe_judgment -> 'a
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 603e909bd..6556b0c76 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -48,11 +48,11 @@ let assumption_of_judgment env j
(* Prop and Set *)
let judge_of_prop =
- { uj_val = mkProp;
+ { uj_val = body_of_type mkProp;
uj_type = mkSort type_0 }
let judge_of_set =
- { uj_val = mkSet;
+ { uj_val = body_of_type mkSet;
uj_type = mkSort type_0 }
let judge_of_prop_contents = function
@@ -63,7 +63,7 @@ let judge_of_prop_contents = function
let judge_of_type u =
let uu = super u in
- { uj_val = mkType u;
+ { uj_val = body_of_type (mkType u);
uj_type = mkType uu }
(*s Type of a de Bruijn index. *)
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-06 12:14:11 +0000