aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--kernel/cbytecodes.ml6
-rw-r--r--kernel/cbytecodes.mli4
-rw-r--r--kernel/cbytegen.ml18
-rw-r--r--kernel/cbytegen.mli4
-rw-r--r--kernel/cemitcodes.ml14
-rw-r--r--kernel/cemitcodes.mli4
-rw-r--r--kernel/conv_oracle.ml10
-rw-r--r--kernel/conv_oracle.mli3
-rw-r--r--kernel/csymtable.ml14
-rw-r--r--kernel/environ.ml4
-rw-r--r--kernel/modops.ml2
-rw-r--r--kernel/names.ml4
-rw-r--r--kernel/names.mli3
-rw-r--r--kernel/nativecode.ml6
-rw-r--r--kernel/nativelambda.ml8
-rw-r--r--kernel/nativelambda.mli2
-rw-r--r--kernel/reduction.ml2
-rw-r--r--kernel/univ.ml2
-rw-r--r--kernel/univ.mli2
-rw-r--r--kernel/vars.ml3
-rw-r--r--kernel/vars.mli3
-rw-r--r--kernel/vconv.ml11
-rw-r--r--kernel/vm.ml13
-rw-r--r--kernel/vm.mli8
-rw-r--r--pretyping/unification.ml4
-rw-r--r--pretyping/vnorm.ml11
-rw-r--r--theories/Init/Datatypes.v4
-rw-r--r--theories/Init/Specif.v8
-rw-r--r--theories/Program/Basics.v4
29 files changed, 94 insertions, 87 deletions
diff --git a/kernel/cbytecodes.ml b/kernel/cbytecodes.ml
index 473a14c24..ae679027d 100644
--- a/kernel/cbytecodes.ml
+++ b/kernel/cbytecodes.ml
@@ -27,7 +27,7 @@ let cofix_evaluated_tag = 6
type structured_constant =
| Const_sorts of sorts
- | Const_ind of inductive
+ | Const_ind of pinductive
| Const_b0 of tag
| Const_bn of tag * structured_constant array
@@ -67,7 +67,7 @@ type instruction =
(* nb fv, init, lbl types, lbl bodies *)
| Kclosurecofix of int * int * Label.t array * Label.t array
(* nb fv, init, lbl types, lbl bodies *)
- | Kgetglobal of constant
+ | Kgetglobal of pconstant
| Kconst of structured_constant
| Kmakeblock of int * tag (* size, tag *)
| Kmakeprod
@@ -185,7 +185,7 @@ let rec instruction ppf = function
Array.iter (fun lbl -> fprintf ppf " %i" lbl) lblt;
print_string " bodies = ";
Array.iter (fun lbl -> fprintf ppf " %i" lbl) lblb;
- | Kgetglobal id -> fprintf ppf "\tgetglobal %s" (Names.string_of_con id)
+ | Kgetglobal (id,u) -> fprintf ppf "\tgetglobal %s" (Names.string_of_con id)
| Kconst cst ->
fprintf ppf "\tconst"
| Kmakeblock(n, m) ->
diff --git a/kernel/cbytecodes.mli b/kernel/cbytecodes.mli
index 225198fcc..b65268f72 100644
--- a/kernel/cbytecodes.mli
+++ b/kernel/cbytecodes.mli
@@ -23,7 +23,7 @@ val cofix_evaluated_tag : tag
type structured_constant =
| Const_sorts of sorts
- | Const_ind of inductive
+ | Const_ind of pinductive
| Const_b0 of tag
| Const_bn of tag * structured_constant array
@@ -60,7 +60,7 @@ type instruction =
(** nb fv, init, lbl types, lbl bodies *)
| Kclosurecofix of int * int * Label.t array * Label.t array
(** nb fv, init, lbl types, lbl bodies *)
- | Kgetglobal of constant
+ | Kgetglobal of pconstant
| Kconst of structured_constant
| Kmakeblock of int * tag (** size, tag *)
| Kmakeprod
diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml
index 39d800737..65ee655da 100644
--- a/kernel/cbytegen.ml
+++ b/kernel/cbytegen.ml
@@ -422,7 +422,7 @@ let rec str_const c =
end
| _ -> Bconstr c
end
- | Ind (ind,u) -> Bstrconst (Const_ind ind)
+ | Ind ind -> Bstrconst (Const_ind ind)
| Construct (((kn,j),i),u) ->
begin
(* spiwack: tries first to apply the run-time compilation
@@ -486,12 +486,12 @@ let rec compile_fv reloc l sz cont =
(* Compiling constants *)
-let rec get_allias env kn =
+let rec get_allias env (kn,u as p) =
let cb = lookup_constant kn env in
let tps = cb.const_body_code in
(match Cemitcodes.force tps with
| BCallias kn' -> get_allias env kn'
- | _ -> kn)
+ | _ -> p)
(* Compiling expressions *)
@@ -700,10 +700,10 @@ and compile_const =
(mkConstU (kn,u)) reloc args sz cont
with Not_found ->
if Int.equal nargs 0 then
- Kgetglobal (get_allias !global_env kn) :: cont
+ Kgetglobal (get_allias !global_env (kn, u)) :: cont
else
comp_app (fun _ _ _ cont ->
- Kgetglobal (get_allias !global_env kn) :: cont)
+ Kgetglobal (get_allias !global_env (kn,u)) :: cont)
compile_constr reloc () args sz cont
let compile env c =
@@ -729,10 +729,10 @@ let compile_constant_body env = function
| Def sb ->
let body = Mod_subst.force_constr sb in
match kind_of_term body with
- | Const kn' ->
+ | Const (kn',u) ->
(* we use the canonical name of the constant*)
- let con= constant_of_kn (canonical_con (Univ.out_punivs kn')) in
- BCallias (get_allias env con)
+ let con= constant_of_kn (canonical_con kn') in
+ BCallias (get_allias env (con,u))
| _ ->
let res = compile env body in
let to_patch = to_memory res in
@@ -740,7 +740,7 @@ let compile_constant_body env = function
(* Shortcut of the previous function used during module strengthening *)
-let compile_alias kn = BCallias (constant_of_kn (canonical_con kn))
+let compile_alias (kn,u) = BCallias (constant_of_kn (canonical_con kn), u)
(* spiwack: additional function which allow different part of compilation of the
31-bit integers *)
diff --git a/kernel/cbytegen.mli b/kernel/cbytegen.mli
index d0bfd46c0..eab36d8b2 100644
--- a/kernel/cbytegen.mli
+++ b/kernel/cbytegen.mli
@@ -13,7 +13,7 @@ val compile_constant_body : env -> constant_def -> body_code
(** Shortcut of the previous function used during module strengthening *)
-val compile_alias : constant -> body_code
+val compile_alias : pconstant -> body_code
(** spiwack: this function contains the information needed to perform
the static compilation of int31 (trying and obtaining
@@ -33,7 +33,7 @@ val dynamic_int31_compilation : bool -> comp_env ->
works as follow: checks if all the arguments are non-pointers
if they are applies the operation (second argument) if not
all of them are, returns to a coq definition (third argument) *)
-val op_compilation : int -> instruction -> constant -> bool -> comp_env ->
+val op_compilation : int -> instruction -> pconstant -> bool -> comp_env ->
constr array -> int -> bytecodes-> bytecodes
(*spiwack: compiling function to insert dynamic decompilation before
diff --git a/kernel/cemitcodes.ml b/kernel/cemitcodes.ml
index 209144044..3c9692a5c 100644
--- a/kernel/cemitcodes.ml
+++ b/kernel/cemitcodes.ml
@@ -20,7 +20,7 @@ open Mod_subst
type reloc_info =
| Reloc_annot of annot_switch
| Reloc_const of structured_constant
- | Reloc_getglobal of constant
+ | Reloc_getglobal of pconstant
type patch = reloc_info * int
@@ -147,8 +147,8 @@ and slot_for_annot a =
enter (Reloc_annot a);
out_int 0
-and slot_for_getglobal id =
- enter (Reloc_getglobal id);
+and slot_for_getglobal p =
+ enter (Reloc_getglobal p);
out_int 0
@@ -320,7 +320,7 @@ let rec subst_strcst s sc =
match sc with
| Const_sorts _ | Const_b0 _ -> sc
| Const_bn(tag,args) -> Const_bn(tag,Array.map (subst_strcst s) args)
- | Const_ind(ind) -> let kn,i = ind in Const_ind((subst_mind s kn, i))
+ | Const_ind(ind,u) -> let kn,i = ind in Const_ind((subst_mind s kn, i), u)
let subst_patch s (ri,pos) =
match ri with
@@ -329,19 +329,19 @@ let subst_patch s (ri,pos) =
let ci = {a.ci with ci_ind = (subst_mind s kn,i)} in
(Reloc_annot {a with ci = ci},pos)
| Reloc_const sc -> (Reloc_const (subst_strcst s sc), pos)
- | Reloc_getglobal kn -> (Reloc_getglobal (fst (subst_con_kn s kn)), pos)
+ | Reloc_getglobal kn -> (Reloc_getglobal (subst_pcon s kn), pos)
let subst_to_patch s (code,pl,fv) =
code,List.rev_map (subst_patch s) pl,fv
type body_code =
| BCdefined of to_patch
- | BCallias of constant
+ | BCallias of pconstant
| BCconstant
let subst_body_code s = function
| BCdefined tp -> BCdefined (subst_to_patch s tp)
- | BCallias kn -> BCallias (fst (subst_con_kn s kn))
+ | BCallias (kn,u) -> BCallias (fst (subst_con_kn s kn), u)
| BCconstant -> BCconstant
type to_patch_substituted = body_code substituted
diff --git a/kernel/cemitcodes.mli b/kernel/cemitcodes.mli
index 287c39304..cec901306 100644
--- a/kernel/cemitcodes.mli
+++ b/kernel/cemitcodes.mli
@@ -4,7 +4,7 @@ open Cbytecodes
type reloc_info =
| Reloc_annot of annot_switch
| Reloc_const of structured_constant
- | Reloc_getglobal of constant
+ | Reloc_getglobal of constant Univ.puniverses
type patch = reloc_info * int
@@ -25,7 +25,7 @@ val subst_to_patch : Mod_subst.substitution -> to_patch -> to_patch
type body_code =
| BCdefined of to_patch
- | BCallias of constant
+ | BCallias of constant Univ.puniverses
| BCconstant
diff --git a/kernel/conv_oracle.ml b/kernel/conv_oracle.ml
index 1c2eea17b..3b01538b9 100644
--- a/kernel/conv_oracle.ml
+++ b/kernel/conv_oracle.ml
@@ -40,12 +40,12 @@ let empty = {
cst_trstate = Cpred.full;
}
-let get_strategy { var_opacity; cst_opacity } = function
+let get_strategy { var_opacity; cst_opacity } f = function
| VarKey id ->
(try Id.Map.find id var_opacity
with Not_found -> default)
| ConstKey c ->
- (try Cmap.find c cst_opacity
+ (try Cmap.find (f c) cst_opacity
with Not_found -> default)
| RelKey _ -> Expand
@@ -83,9 +83,11 @@ let get_transp_state { var_trstate; cst_trstate } = (var_trstate, cst_trstate)
(* Unfold the first constant only if it is "more transparent" than the
second one. In case of tie, expand the second one. *)
-let oracle_order o l2r k1 k2 =
- match get_strategy o k1, get_strategy o k2 with
+let oracle_order f o l2r k1 k2 =
+ match get_strategy o f k1, get_strategy o f k2 with
| Expand, _ -> true
| Level n1, Opaque -> true
| Level n1, Level n2 -> n1 < n2
| _ -> l2r (* use recommended default *)
+
+let get_strategy o = get_strategy o (fun x -> x)
diff --git a/kernel/conv_oracle.mli b/kernel/conv_oracle.mli
index 550076782..629912220 100644
--- a/kernel/conv_oracle.mli
+++ b/kernel/conv_oracle.mli
@@ -16,7 +16,8 @@ val empty : oracle
If [oracle_order kn1 kn2] is true, then unfold kn1 first.
Note: the oracle does not introduce incompleteness, it only
tries to postpone unfolding of "opaque" constants. *)
-val oracle_order : oracle -> bool -> constant tableKey -> constant tableKey -> bool
+val oracle_order : ('a -> constant) -> oracle -> bool ->
+ 'a tableKey -> 'a tableKey -> bool
(** Priority for the expansion of constant in the conversion test.
* Higher levels means that the expansion is less prioritary.
diff --git a/kernel/csymtable.ml b/kernel/csymtable.ml
index 794d94581..ed8b0a6d1 100644
--- a/kernel/csymtable.ml
+++ b/kernel/csymtable.ml
@@ -57,7 +57,7 @@ let set_global v =
let rec eq_structured_constant c1 c2 = match c1, c2 with
| Const_sorts s1, Const_sorts s2 -> Sorts.equal s1 s2
-| Const_ind i1, Const_ind i2 -> eq_ind i1 i2
+| Const_ind i1, Const_ind i2 -> Univ.eq_puniverses eq_ind i1 i2
| Const_b0 t1, Const_b0 t2 -> Int.equal t1 t2
| Const_bn (t1, a1), Const_bn (t2, a2) ->
Int.equal t1 t2 && Array.equal eq_structured_constant a1 a2
@@ -67,7 +67,7 @@ let rec hash_structured_constant c =
let open Hashset.Combine in
match c with
| Const_sorts s -> combinesmall 1 (Sorts.hash s)
- | Const_ind i -> combinesmall 2 (ind_hash i)
+ | Const_ind (i,u) -> combinesmall 2 (combine (ind_hash i) (Univ.Instance.hash u))
| Const_b0 t -> combinesmall 3 (Int.hash t)
| Const_bn (t, a) ->
let fold h c = combine h (hash_structured_constant c) in
@@ -142,7 +142,7 @@ let slot_for_annot key =
AnnotTable.add annot_tbl key n;
n
-let rec slot_for_getglobal env kn =
+let rec slot_for_getglobal env (kn,u) =
let (cb,(_,rk)) = lookup_constant_key kn env in
try key rk
with NotEvaluated ->
@@ -150,10 +150,12 @@ let rec slot_for_getglobal env kn =
let pos =
match Cemitcodes.force cb.const_body_code with
| BCdefined(code,pl,fv) ->
- let v = eval_to_patch env (code,pl,fv) in
- set_global v
+ if Univ.Instance.is_empty u then
+ let v = eval_to_patch env (code,pl,fv) in
+ set_global v
+ else set_global (val_of_constant (kn,u))
| BCallias kn' -> slot_for_getglobal env kn'
- | BCconstant -> set_global (val_of_constant kn) in
+ | BCconstant -> set_global (val_of_constant (kn,u)) in
(*Pp.msgnl(str"value stored at: "++int pos);*)
rk := Some (Ephemeron.create pos);
pos
diff --git a/kernel/environ.ml b/kernel/environ.ml
index 8b1e49919..0ebff440a 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -594,7 +594,7 @@ let dispatch =
let int31_op n op prim kn =
{ empty_reactive_info with
vm_compiling = Some (Cbytegen.op_compilation n op kn);
- native_compiling = Some (Nativelambda.compile_prim prim kn);
+ native_compiling = Some (Nativelambda.compile_prim prim (Univ.out_punivs kn));
}
in
@@ -602,7 +602,7 @@ fun rk value field ->
(* subfunction which shortens the (very common) dispatch of operations *)
let int31_op_from_const n op prim =
match kind_of_term value with
- | Const (kn,_) -> int31_op n op prim kn
+ | Const kn -> int31_op n op prim kn
| _ -> anomaly ~label:"Environ.register" (Pp.str "should be a constant")
in
let int31_binop_from_const op prim = int31_op_from_const 2 op prim in
diff --git a/kernel/modops.ml b/kernel/modops.ml
index e04eb354e..392e667b8 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -337,7 +337,7 @@ let strengthen_const mp_from l cb resolver =
in
{ cb with
const_body = Def (Mod_subst.from_val (mkConstU (con,u)));
- const_body_code = Cemitcodes.from_val (Cbytegen.compile_alias con) }
+ const_body_code = Cemitcodes.from_val (Cbytegen.compile_alias (con,u)) }
let rec strengthen_mod mp_from mp_to mb =
if mp_in_delta mb.mod_mp mb.mod_delta then mb
diff --git a/kernel/names.ml b/kernel/names.ml
index 2c2886623..b349ccb00 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -686,8 +686,6 @@ type inv_rel_key = int (* index in the [rel_context] part of environment
starting by the end, {\em inverse}
of de Bruijn indice *)
-type id_key = Constant.t tableKey
-
let eq_table_key f ik1 ik2 =
if ik1 == ik2 then true
else match ik1,ik2 with
@@ -696,8 +694,6 @@ let eq_table_key f ik1 ik2 =
| RelKey k1, RelKey k2 -> Int.equal k1 k2
| _ -> false
-let eq_id_key = eq_table_key Constant.UserOrd.equal
-
let eq_con_chk = Constant.UserOrd.equal
let eq_mind_chk = MutInd.UserOrd.equal
let eq_ind_chk (kn1,i1) (kn2,i2) = Int.equal i1 i2 && eq_mind_chk kn1 kn2
diff --git a/kernel/names.mli b/kernel/names.mli
index 9fbe7d5e5..d82043da1 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -458,11 +458,8 @@ type inv_rel_key = int (** index in the [rel_context] part of environment
starting by the end, {e inverse}
of de Bruijn indice *)
-type id_key = Constant.t tableKey
-
val eq_table_key : ('a -> 'a -> bool) -> 'a tableKey -> 'a tableKey -> bool
val eq_constant_key : Constant.t -> Constant.t -> bool
-val eq_id_key : id_key -> id_key -> bool
(** equalities on constant and inductive names (for the checker) *)
diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml
index 433e2c505..66577fecc 100644
--- a/kernel/nativecode.ml
+++ b/kernel/nativecode.ml
@@ -1772,7 +1772,7 @@ let compile_constant env sigma prefix ~interactive con cb =
match cb.const_proj with
| None ->
begin match cb.const_body with
- | Def t ->
+ | Def t when not cb.const_polymorphic ->
let t = Mod_subst.force_constr t in
let code = lambda_of_constr env sigma t in
if !Flags.debug then Pp.msg_debug (Pp.str "Generated lambda code");
@@ -1902,8 +1902,8 @@ let compile_mind_deps env prefix ~interactive
let rec compile_deps env sigma prefix ~interactive init t =
match kind_of_term t with
| Ind ((mind,_),u) -> compile_mind_deps env prefix ~interactive init mind
- | Const (c,u) ->
- let c = get_allias env c in
+ | Const c ->
+ let c,u = get_allias env c in
let cb,(nameref,_) = lookup_constant_key c env in
let (_, (_, const_updates)) = init in
if is_code_loaded ~interactive nameref
diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml
index c5417b2b6..947e0a148 100644
--- a/kernel/nativelambda.ml
+++ b/kernel/nativelambda.ml
@@ -373,11 +373,11 @@ let makeblock env cn tag args =
(* Translation of constants *)
-let rec get_allias env kn =
+let rec get_allias env (kn, u as p) =
let tps = (lookup_constant kn env).const_body_code in
match Cemitcodes.force tps with
| Cemitcodes.BCallias kn' -> get_allias env kn'
- | _ -> kn
+ | _ -> p
(*i Global environment *)
@@ -647,8 +647,8 @@ let rec lambda_of_constr env sigma c =
and lambda_of_app env sigma f args =
match kind_of_term f with
- | Const (kn,u) ->
- let kn = get_allias !global_env kn in
+ | Const (kn,u as c) ->
+ let kn,u = get_allias !global_env c in
let cb = lookup_constant kn !global_env in
(try
let prefix = get_const_prefix !global_env kn in
diff --git a/kernel/nativelambda.mli b/kernel/nativelambda.mli
index 10818e1aa..6a97edc40 100644
--- a/kernel/nativelambda.mli
+++ b/kernel/nativelambda.mli
@@ -27,7 +27,7 @@ val mk_lazy : lambda -> lambda
val get_mind_prefix : env -> mutual_inductive -> string
-val get_allias : env -> constant -> constant
+val get_allias : env -> pconstant -> pconstant
val lambda_of_constr : env -> evars -> Constr.constr -> lambda
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 62f454047..4153b323b 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -350,7 +350,7 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
(* else the oracle tells which constant is to be expanded *)
let oracle = Closure.oracle_of_infos infos in
let (app1,app2) =
- if Conv_oracle.oracle_order oracle l2r (conv_key fl1) (conv_key fl2) then
+ if Conv_oracle.oracle_order Univ.out_punivs oracle l2r fl1 fl2 then
match unfold_reference infos fl1 with
| Some def1 -> ((lft1, whd def1 v1), appr2)
| None ->
diff --git a/kernel/univ.ml b/kernel/univ.ml
index d5939c67e..e2a19b0e8 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -1744,6 +1744,8 @@ type universe_instance = Instance.t
type 'a puniverses = 'a * Instance.t
let out_punivs (x, y) = x
let in_punivs x = (x, Instance.empty)
+let eq_puniverses f (x, u) (y, u') =
+ f x y && Instance.equal u u'
(** A context of universe levels with universe constraints,
representiong local universe variables and constraints *)
diff --git a/kernel/univ.mli b/kernel/univ.mli
index 36f3349c0..454134f21 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -306,6 +306,8 @@ type 'a puniverses = 'a * universe_instance
val out_punivs : 'a puniverses -> 'a
val in_punivs : 'a -> 'a puniverses
+val eq_puniverses : ('a -> 'a -> bool) -> 'a puniverses -> 'a puniverses -> bool
+
(** A vector of universe levels with universe constraints,
representiong local universe variables and associated constraints *)
diff --git a/kernel/vars.ml b/kernel/vars.ml
index 1685817a3..88c1e1038 100644
--- a/kernel/vars.ml
+++ b/kernel/vars.ml
@@ -336,3 +336,6 @@ let subst_instance_constr subst c =
let subst_instance_context s ctx =
if Univ.Instance.is_empty s then ctx
else map_rel_context (fun x -> subst_instance_constr s x) ctx
+
+type id_key = pconstant tableKey
+let eq_id_key x y = Names.eq_table_key (Univ.eq_puniverses Constant.equal) x y
diff --git a/kernel/vars.mli b/kernel/vars.mli
index bdbecdedc..fdd4603b5 100644
--- a/kernel/vars.mli
+++ b/kernel/vars.mli
@@ -87,3 +87,6 @@ val subst_univs_level_context : Univ.universe_level_subst -> rel_context -> rel_
(** Instance substitution for polymorphism. *)
val subst_instance_constr : universe_instance -> constr -> constr
val subst_instance_context : universe_instance -> rel_context -> rel_context
+
+type id_key = pconstant tableKey
+val eq_id_key : id_key -> id_key -> bool
diff --git a/kernel/vconv.ml b/kernel/vconv.ml
index 3f9345ff8..80b15f8ba 100644
--- a/kernel/vconv.ml
+++ b/kernel/vconv.ml
@@ -86,23 +86,24 @@ and conv_whd env pb k whd1 whd2 cu =
and conv_atom env pb k a1 stk1 a2 stk2 cu =
match a1, a2 with
- | Aind (kn1,i1), Aind(kn2,i2) ->
- if eq_ind (kn1,i1) (kn2,i2) && compare_stack stk1 stk2
+ | Aind ind1, Aind ind2 ->
+ if eq_puniverses eq_ind ind1 ind2 && compare_stack stk1 stk2
then
conv_stack env k stk1 stk2 cu
else raise NotConvertible
| Aid ik1, Aid ik2 ->
- if eq_id_key ik1 ik2 && compare_stack stk1 stk2 then
+ if Vars.eq_id_key ik1 ik2 && compare_stack stk1 stk2 then
conv_stack env k stk1 stk2 cu
else raise NotConvertible
| Aiddef(ik1,v1), Aiddef(ik2,v2) ->
begin
try
- if eq_table_key ik1 ik2 && compare_stack stk1 stk2 then
+ if Vars.eq_id_key ik1 ik2 && compare_stack stk1 stk2 then
conv_stack env k stk1 stk2 cu
else raise NotConvertible
with NotConvertible ->
- if oracle_order (oracle_of_infos !infos) false ik1 ik2 then
+ if oracle_order Univ.out_punivs (oracle_of_infos !infos)
+ false ik1 ik2 then
conv_whd env pb k (whd_stack v1 stk1) (Vatom_stk(a2,stk2)) cu
else conv_whd env pb k (Vatom_stk(a1,stk1)) (whd_stack v2 stk2) cu
end
diff --git a/kernel/vm.ml b/kernel/vm.ml
index a7e5a55c4..2cc1efe43 100644
--- a/kernel/vm.ml
+++ b/kernel/vm.ml
@@ -137,10 +137,11 @@ type vswitch = {
(* Generally the first field is a code pointer. *)
(* Do not edit this type without editing C code, especially "coq_values.h" *)
+
type atom =
- | Aid of id_key
- | Aiddef of id_key * values
- | Aind of inductive
+ | Aid of Vars.id_key
+ | Aiddef of Vars.id_key * values
+ | Aind of pinductive
(* Zippers *)
@@ -306,11 +307,11 @@ let val_of_atom a = val_of_obj (obj_of_atom a)
module IdKeyHash =
struct
- type t = id_key
- let equal = Names.eq_id_key
+ type t = pconstant tableKey
+ let equal = Names.eq_table_key (Univ.eq_puniverses Constant.equal)
open Hashset.Combine
let hash = function
- | ConstKey c -> combinesmall 1 (Constant.hash c)
+ | ConstKey (c,u) -> combinesmall 1 (Constant.hash c)
| VarKey id -> combinesmall 2 (Id.hash id)
| RelKey i -> combinesmall 3 (Int.hash i)
end
diff --git a/kernel/vm.mli b/kernel/vm.mli
index fa88418ce..295ea83c4 100644
--- a/kernel/vm.mli
+++ b/kernel/vm.mli
@@ -24,9 +24,9 @@ type vswitch
type arguments
type atom =
- | Aid of id_key
- | Aiddef of id_key * values
- | Aind of inductive
+ | Aid of Vars.id_key
+ | Aiddef of Vars.id_key * values
+ | Aind of pinductive
(** Zippers *)
@@ -54,7 +54,7 @@ type whd =
val val_of_str_const : structured_constant -> values
val val_of_rel : int -> values
val val_of_named : Id.t -> values
-val val_of_constant : constant -> values
+val val_of_constant : pconstant -> values
external val_of_annot_switch : annot_switch -> values = "%identity"
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 3f9f7ff28..203b1ec8a 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -511,8 +511,8 @@ let oracle_order env cf1 cf2 =
when eq_constant p (Projection.constant p') ->
Some (Projection.unfolded p')
| _ ->
- Some (Conv_oracle.oracle_order (Environ.oracle env) false
- (translate_key k1) (translate_key k2))
+ Some (Conv_oracle.oracle_order (fun x -> x)
+ (Environ.oracle env) false (translate_key k1) (translate_key k2))
let is_rigid_head flags t =
match kind_of_term t with
diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml
index 1d97aef27..3f1e6e5d6 100644
--- a/pretyping/vnorm.ml
+++ b/pretyping/vnorm.ml
@@ -93,12 +93,11 @@ let construct_of_constr_const env tag typ =
let construct_of_constr_block = construct_of_constr false
-(* FIXME: treatment of universes *)
let constr_type_of_idkey env idkey =
match idkey with
| ConstKey cst ->
- let const_type = (Environ.lookup_constant cst env).const_type in
- mkConst cst, Typeops.type_of_constant_type env const_type
+ let const_type = Typeops.type_of_constant_in env cst in
+ mkConstU cst, const_type
| VarKey id ->
let (_,_,ty) = lookup_named id env in
mkVar id, ty
@@ -107,7 +106,7 @@ let constr_type_of_idkey env idkey =
let (_,_,ty) = lookup_rel n env in
mkRel n, lift n ty
-let type_of_ind env ind u =
+let type_of_ind env (ind, u) =
type_of_inductive env (Inductive.lookup_mind_specif env ind, u)
let build_branches_type env (mind,_ as _ind) mib mip u params dep p =
@@ -176,7 +175,7 @@ and nf_whd env whd typ =
| Vatom_stk(Aiddef(idkey,v), stk) ->
nf_whd env (whd_stack v stk) typ
| Vatom_stk(Aind ind, stk) ->
- nf_stk env (mkInd ind) (type_of_ind env ind Univ.Instance.empty (*FIXME*)) stk
+ nf_stk env (mkIndU ind) (type_of_ind env ind) stk
and nf_stk env c t stk =
match stk with
@@ -194,7 +193,7 @@ and nf_stk env c t stk =
let nparams = mib.mind_nparams in
let params,realargs = Util.Array.chop nparams allargs in
let pT =
- hnf_prod_applist env (type_of_ind env ind u) (Array.to_list params) in
+ hnf_prod_applist env (type_of_ind env (ind,u)) (Array.to_list params) in
let pT = whd_betadeltaiota env pT in
let dep, p = nf_predicate env ind mip params (type_of_switch sw) pT in
(* Calcul du type des branches *)
diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v
index a04535f40..de615301d 100644
--- a/theories/Init/Datatypes.v
+++ b/theories/Init/Datatypes.v
@@ -342,8 +342,8 @@ Arguments identity_rect [A] a P f y i.
(** Identity type *)
-Polymorphic Definition ID := forall A:Type, A -> A.
-Polymorphic Definition id : ID := fun A x => x.
+Definition ID := forall A:Type, A -> A.
+Definition id : ID := fun A x => x.
Definition IDProp := forall A:Prop, A -> A.
Definition idProp : IDProp := fun A x => x.
diff --git a/theories/Init/Specif.v b/theories/Init/Specif.v
index 47e302e32..1384901b7 100644
--- a/theories/Init/Specif.v
+++ b/theories/Init/Specif.v
@@ -21,19 +21,19 @@ Require Import Logic.
Similarly [(sig2 A P Q)], or [{x:A | P x & Q x}], denotes the subset
of elements of the type [A] which satisfy both [P] and [Q]. *)
-(* Polymorphic *) Inductive sig (A:Type) (P:A -> Prop) : Type :=
+Inductive sig (A:Type) (P:A -> Prop) : Type :=
exist : forall x:A, P x -> sig P.
-(* Polymorphic *) Inductive sig2 (A:Type) (P Q:A -> Prop) : Type :=
+Inductive sig2 (A:Type) (P Q:A -> Prop) : Type :=
exist2 : forall x:A, P x -> Q x -> sig2 P Q.
(** [(sigT A P)], or more suggestively [{x:A & (P x)}] is a Sigma-type.
Similarly for [(sigT2 A P Q)], also written [{x:A & (P x) & (Q x)}]. *)
-(* Polymorphic *) Inductive sigT (A:Type) (P:A -> Type) : Type :=
+Inductive sigT (A:Type) (P:A -> Type) : Type :=
existT : forall x:A, P x -> sigT P.
-(* Polymorphic *) Inductive sigT2 (A:Type) (P Q:A -> Type) : Type :=
+Inductive sigT2 (A:Type) (P Q:A -> Type) : Type :=
existT2 : forall x:A, P x -> Q x -> sigT2 P Q.
(* Notations *)
diff --git a/theories/Program/Basics.v b/theories/Program/Basics.v
index 4bc29a071..e5be0ca92 100644
--- a/theories/Program/Basics.v
+++ b/theories/Program/Basics.v
@@ -15,8 +15,6 @@
Institution: LRI, CNRS UMR 8623 - University Paris Sud
*)
-(* Set Universe Polymorphism. *)
-
(** The polymorphic identity function is defined in [Datatypes]. *)
Arguments id {A} x.
@@ -47,7 +45,7 @@ Definition const {A B} (a : A) := fun _ : B => a.
(** The [flip] combinator reverses the first two arguments of a function. *)
-Monomorphic Definition flip {A B C} (f : A -> B -> C) x y := f y x.
+Definition flip {A B C} (f : A -> B -> C) x y := f y x.
(** Application as a combinator. *)
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-29 09:02:56 +0000