aboutsummaryrefslogtreecommitdiffhomepage
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/inductiveops.ml24
-rw-r--r--pretyping/inductiveops.mli12
-rw-r--r--pretyping/nativenorm.ml2
-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.ml11
-rw-r--r--pretyping/vnorm.ml2
13 files changed, 40 insertions, 50 deletions
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index bf9e37aa7..5c4cbefad 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 2bc603a90..d7118efd7 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 23a985dc3..d0de2f8c0 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 8afb9b942..3f5d186d4 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/inductiveops.ml b/pretyping/inductiveops.ml
index d599afe69..576073344 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 aa53f7e67..8eaef24c4 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 7319846fb..16d003f67 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 ->
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index 622a8e982..685aa400b 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 746a68b21..7e43c5e41 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 d3aa7ac64..efb3c339a 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 e4a56960c..80c6d8239 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 cf34ac016..a66ecaaac 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -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 14c9f49b1..bd6062824 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)
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-05 19:59:55 +0000