aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--interp/constrintern.ml22
-rw-r--r--intf/constrexpr.mli6
-rw-r--r--intf/glob_term.mli2
-rw-r--r--kernel/environ.ml12
-rw-r--r--kernel/fast_typeops.ml4
-rw-r--r--kernel/inductive.ml12
-rw-r--r--kernel/inductive.mli5
-rw-r--r--kernel/typeops.ml4
-rw-r--r--kernel/univ.ml12
-rw-r--r--kernel/univ.mli9
-rw-r--r--kernel/vars.ml4
-rw-r--r--kernel/vars.mli6
-rw-r--r--library/universes.ml73
-rw-r--r--library/universes.mli14
-rw-r--r--parsing/g_constr.ml410
-rw-r--r--pretyping/detyping.ml15
-rw-r--r--pretyping/evd.ml77
-rw-r--r--pretyping/evd.mli13
-rw-r--r--pretyping/indrec.ml4
-rw-r--r--pretyping/inductiveops.ml10
-rw-r--r--pretyping/pretyping.ml42
-rw-r--r--pretyping/vnorm.ml2
-rw-r--r--printing/ppconstr.ml2
-rw-r--r--tactics/eqschemes.ml14
-rw-r--r--test-suite/success/polymorphism.v27
25 files changed, 275 insertions, 126 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index d8cf9fd16..7f13fff2c 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -748,9 +748,9 @@ let intern_reference ref =
Smartlocate.global_of_extended_global r
(* Is it a global reference or a syntactic definition? *)
-let intern_qualid loc qid intern env lvar args =
+let intern_qualid loc qid intern env lvar us args =
match intern_extended_global_of_qualid (loc,qid) with
- | TrueGlobal ref -> GRef (loc, ref, None), args
+ | TrueGlobal ref -> GRef (loc, ref, us), args
| SynDef sp ->
let (ids,c) = Syntax_def.search_syntactic_definition sp in
let nids = List.length ids in
@@ -763,15 +763,15 @@ let intern_qualid loc qid intern env lvar args =
subst_aconstr_in_glob_constr loc intern lvar subst infos c, args2
(* Rule out section vars since these should have been found by intern_var *)
-let intern_non_secvar_qualid loc qid intern env lvar args =
- match intern_qualid loc qid intern env lvar args with
+let intern_non_secvar_qualid loc qid intern env lvar us args =
+ match intern_qualid loc qid intern env lvar us args with
| GRef (_, VarRef _, _),_ -> raise Not_found
| r -> r
-let intern_applied_reference intern env namedctx lvar args = function
+let intern_applied_reference intern env namedctx lvar us args = function
| Qualid (loc, qid) ->
let r,args2 =
- try intern_qualid loc qid intern env lvar args
+ try intern_qualid loc qid intern env lvar us args
with Not_found -> error_global_not_found_loc loc qid
in
let x, isproj, imp, scopes, l = find_appl_head_data r in
@@ -781,7 +781,7 @@ let intern_applied_reference intern env namedctx lvar args = function
with Not_found ->
let qid = qualid_of_ident id in
try
- let r,args2 = intern_non_secvar_qualid loc qid intern env lvar args in
+ let r,args2 = intern_non_secvar_qualid loc qid intern env lvar us args in
let x, isproj, imp, scopes, l = find_appl_head_data r in
(x,imp,scopes,l), isproj, args2
with Not_found ->
@@ -795,7 +795,7 @@ let interp_reference vars r =
intern_applied_reference (fun _ -> error_not_enough_arguments Loc.ghost)
{ids = Id.Set.empty; unb = false ;
tmp_scope = None; scopes = []; impls = empty_internalization_env} []
- (vars, Id.Map.empty) [] r
+ (vars, Id.Map.empty) None [] r
in r
(**********************************************************************)
@@ -1368,7 +1368,7 @@ let internalize globalenv env allow_patvar lvar c =
let rec intern env = function
| CRef (ref,us) as x ->
let (c,imp,subscopes,l),isproj,_ =
- intern_applied_reference intern env (Environ.named_context globalenv) lvar [] ref in
+ intern_applied_reference intern env (Environ.named_context globalenv) lvar us [] ref in
apply_impargs (None, isproj) c env imp subscopes l (constr_loc x)
| CFix (loc, (locid,iddef), dl) ->
@@ -1467,7 +1467,7 @@ let internalize globalenv env allow_patvar lvar c =
let (f,_,args_scopes,_),_,args =
let args = List.map (fun a -> (a,None)) args in
intern_applied_reference intern env (Environ.named_context globalenv)
- lvar args ref in
+ lvar us args ref in
(* check_projection isproj (List.length args) f; *)
(* Rem: GApp(_,f,[]) stands for @f *)
GApp (loc, f, intern_args env args_scopes (List.map fst args))
@@ -1483,7 +1483,7 @@ let internalize globalenv env allow_patvar lvar c =
match f with
| CRef (ref,us) ->
intern_applied_reference intern env
- (Environ.named_context globalenv) lvar args ref
+ (Environ.named_context globalenv) lvar us args ref
| CNotation (loc,ntn,([],[],[])) ->
let c = intern_notation intern env lvar loc ntn ([],[],[]) in
let x, isproj, impl, scopes, l = find_appl_head_data c in
diff --git a/intf/constrexpr.mli b/intf/constrexpr.mli
index af6aea164..c28c4dcb1 100644
--- a/intf/constrexpr.mli
+++ b/intf/constrexpr.mli
@@ -61,14 +61,16 @@ and cases_pattern_notation_substitution =
cases_pattern_expr list * (** for constr subterms *)
cases_pattern_expr list list (** for recursive notations *)
+type instance_expr = Misctypes.glob_sort list
+
type constr_expr =
- | CRef of reference * Univ.universe_instance option
+ | CRef of reference * instance_expr option
| CFix of Loc.t * Id.t located * fix_expr list
| CCoFix of Loc.t * Id.t located * cofix_expr list
| CProdN of Loc.t * binder_expr list * constr_expr
| CLambdaN of Loc.t * binder_expr list * constr_expr
| CLetIn of Loc.t * Name.t located * constr_expr * constr_expr
- | CAppExpl of Loc.t * (proj_flag * reference * Univ.universe_instance option) * constr_expr list
+ | CAppExpl of Loc.t * (proj_flag * reference * instance_expr option) * constr_expr list
| CApp of Loc.t * (proj_flag * constr_expr) *
(constr_expr * explicitation located option) list
| CRecord of Loc.t * constr_expr option * (reference * constr_expr) list
diff --git a/intf/glob_term.mli b/intf/glob_term.mli
index d07766e18..d37955225 100644
--- a/intf/glob_term.mli
+++ b/intf/glob_term.mli
@@ -28,7 +28,7 @@ type cases_pattern =
(** [PatCstr(p,C,l,x)] = "|'C' 'l' as 'x'" *)
type glob_constr =
- | GRef of (Loc.t * global_reference * Univ.universe_instance option)
+ | GRef of (Loc.t * global_reference * glob_sort list option)
| GVar of (Loc.t * Id.t)
| GEvar of Loc.t * existential_key * glob_constr list option
| GPatVar of Loc.t * (bool * patvar) (** Used for patterns only *)
diff --git a/kernel/environ.ml b/kernel/environ.ml
index 7a90f3675..f4420c489 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -229,7 +229,7 @@ let constant_type env (kn,u) =
let cb = lookup_constant kn env in
if cb.const_polymorphic then
let subst, csts = universes_and_subst_of cb u in
- (map_regular_arity (subst_univs_constr subst) cb.const_type, csts)
+ (map_regular_arity (subst_univs_level_constr subst) cb.const_type, csts)
else cb.const_type, Univ.Constraint.empty
let constant_context env kn =
@@ -248,7 +248,7 @@ let constant_value env (kn,u) =
| Def l_body ->
if cb.const_polymorphic then
let subst, csts = universes_and_subst_of cb u in
- (subst_univs_constr subst (Mod_subst.force_constr l_body), csts)
+ (subst_univs_level_constr subst (Mod_subst.force_constr l_body), csts)
else Mod_subst.force_constr l_body, Univ.Constraint.empty
| OpaqueDef _ -> raise (NotEvaluableConst Opaque)
| Undef _ -> raise (NotEvaluableConst NoBody)
@@ -263,11 +263,11 @@ let constant_value_and_type env (kn, u) =
if cb.const_polymorphic then
let subst, cst = universes_and_subst_of cb u in
let b' = match cb.const_body with
- | Def l_body -> Some (subst_univs_constr subst (Mod_subst.force_constr l_body))
+ | Def l_body -> Some (subst_univs_level_constr subst (Mod_subst.force_constr l_body))
| OpaqueDef _ -> None
| Undef _ -> None
in
- b', map_regular_arity (subst_univs_constr subst) cb.const_type, cst
+ b', map_regular_arity (subst_univs_level_constr subst) cb.const_type, cst
else
let b' = match cb.const_body with
| Def l_body -> Some (Mod_subst.force_constr l_body)
@@ -284,7 +284,7 @@ let constant_type_in env (kn,u) =
let cb = lookup_constant kn env in
if cb.const_polymorphic then
let subst = Univ.make_universe_subst u cb.const_universes in
- map_regular_arity (subst_univs_constr subst) cb.const_type
+ map_regular_arity (subst_univs_level_constr subst) cb.const_type
else cb.const_type
let constant_value_in env (kn,u) =
@@ -294,7 +294,7 @@ let constant_value_in env (kn,u) =
let b = Mod_subst.force_constr l_body in
if cb.const_polymorphic then
let subst = Univ.make_universe_subst u cb.const_universes in
- subst_univs_constr subst b
+ subst_univs_level_constr subst b
else b
| OpaqueDef _ -> raise (NotEvaluableConst Opaque)
| Undef _ -> raise (NotEvaluableConst NoBody)
diff --git a/kernel/fast_typeops.ml b/kernel/fast_typeops.ml
index 6d48aaa4e..94e4479d2 100644
--- a/kernel/fast_typeops.ml
+++ b/kernel/fast_typeops.ml
@@ -149,7 +149,7 @@ let type_of_projection env (cst,u) =
if cb.const_polymorphic then
let mib,_ = lookup_mind_specif env (pb.proj_ind,0) in
let subst = make_inductive_subst mib u in
- Vars.subst_univs_constr subst pb.proj_type
+ Vars.subst_univs_level_constr subst pb.proj_type
else pb.proj_type
| None -> raise (Invalid_argument "type_of_projection: not a projection")
@@ -333,7 +333,7 @@ let judge_of_projection env p c ct =
in
assert(eq_mind pb.proj_ind (fst ind));
let usubst = make_inductive_subst (fst (lookup_mind_specif env ind)) u in
- let ty = Vars.subst_univs_constr usubst pb.Declarations.proj_type in
+ let ty = Vars.subst_univs_level_constr usubst pb.Declarations.proj_type in
substl (c :: List.rev args) ty
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 3f1c4e75f..f07217ac0 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -56,11 +56,11 @@ let inductive_params (mib,_) = mib.mind_nparams
let make_inductive_subst mib u =
if mib.mind_polymorphic then
make_universe_subst u mib.mind_universes
- else Univ.empty_subst
+ else Univ.empty_level_subst
let inductive_params_ctxt (mib,u) =
let subst = make_inductive_subst mib u in
- Vars.subst_univs_context subst mib.mind_params_ctxt
+ Vars.subst_univs_level_context subst mib.mind_params_ctxt
let inductive_instance mib =
if mib.mind_polymorphic then
@@ -89,7 +89,7 @@ let ind_subst mind mib u =
(* Instantiate inductives in constructor type *)
let constructor_instantiate mind u subst mib c =
let s = ind_subst mind mib u in
- substl s (subst_univs_constr subst c)
+ substl s (subst_univs_level_constr subst c)
let instantiate_params full t args sign =
let fail () =
@@ -113,7 +113,7 @@ let full_inductive_instantiate mib u params sign =
let t = mkArity (sign,dummy) in
let subst = make_inductive_subst mib u in
let ar = fst (destArity (instantiate_params true t params mib.mind_params_ctxt)) in
- Vars.subst_univs_context subst ar
+ Vars.subst_univs_level_context subst ar
let full_constructor_instantiate ((mind,_),u,(mib,_),params) =
let subst = make_inductive_subst mib u in
@@ -217,7 +217,7 @@ let type_of_inductive_subst ?(polyprop=true) env ((mib,mip),u) paramtyps =
if not mib.mind_polymorphic then (a.mind_user_arity, Univ.LMap.empty)
else
let subst = make_inductive_subst mib u in
- (subst_univs_constr subst a.mind_user_arity, subst)
+ (subst_univs_level_constr subst a.mind_user_arity, subst)
| TemplateArity ar ->
let ctx = List.rev mip.mind_arity_ctxt in
let ctx,s = instantiate_universes env ctx ar paramtyps in
@@ -234,7 +234,7 @@ let type_of_inductive_gen ?(polyprop=true) env ((mib,mip),u) paramtyps =
if not mib.mind_polymorphic then a.mind_user_arity
else
let subst = make_inductive_subst mib u in
- (subst_univs_constr subst a.mind_user_arity)
+ (subst_univs_level_constr subst a.mind_user_arity)
| TemplateArity ar ->
let ctx = List.rev mip.mind_arity_ctxt in
let ctx,s = instantiate_universes env ctx ar paramtyps in
diff --git a/kernel/inductive.mli b/kernel/inductive.mli
index a23d170f5..497c06417 100644
--- a/kernel/inductive.mli
+++ b/kernel/inductive.mli
@@ -35,13 +35,14 @@ val lookup_mind_specif : env -> inductive -> mind_specif
(** {6 Functions to build standard types related to inductive } *)
val ind_subst : mutual_inductive -> mutual_inductive_body -> universe_instance -> constr list
-val make_inductive_subst : mutual_inductive_body -> universe_instance -> universe_subst
+val make_inductive_subst : mutual_inductive_body -> universe_instance -> universe_level_subst
val inductive_instance : mutual_inductive_body -> universe_instance
val inductive_context : mutual_inductive_body -> universe_context
val inductive_params_ctxt : mutual_inductive_body puniverses -> rel_context
-val instantiate_inductive_constraints : mutual_inductive_body -> universe_subst -> constraints
+val instantiate_inductive_constraints :
+ mutual_inductive_body -> universe_level_subst -> constraints
val constrained_type_of_inductive : env -> mind_specif puniverses -> types constrained
val constrained_type_of_inductive_knowing_parameters :
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 49f883628..98c0dfc20 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -176,7 +176,7 @@ let type_of_projection env (cst,u) =
if cb.const_polymorphic then
let mib,_ = lookup_mind_specif env (pb.proj_ind,0) in
let subst = make_inductive_subst mib u in
- Vars.subst_univs_constr subst pb.proj_type
+ Vars.subst_univs_level_constr subst pb.proj_type
else pb.proj_type
| None -> raise (Invalid_argument "type_of_projection: not a projection")
@@ -374,7 +374,7 @@ let judge_of_projection env p cj =
in
assert(eq_mind pb.proj_ind (fst ind));
let usubst = make_inductive_subst (fst (lookup_mind_specif env ind)) u in
- let ty = Vars.subst_univs_constr usubst pb.Declarations.proj_type in
+ let ty = Vars.subst_univs_level_constr usubst pb.Declarations.proj_type in
let ty = substl (cj.uj_val :: List.rev args) ty in
(* TODO: Universe polymorphism for projections *)
{uj_val = mkProj (p,cj.uj_val);
diff --git a/kernel/univ.ml b/kernel/univ.ml
index 8984938d3..147efe86b 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -454,7 +454,13 @@ module Level = struct
let hcons = hashcons
let equal = deep_equal (* Not shallow as serialization breaks sharing *)
- let hash = Hashtbl.hash
+
+ open Hashset.Combine
+
+ let hash = function
+ | Prop -> combinesmall 1 0
+ | Set -> combinesmall 1 1
+ | Level (n, d) -> combinesmall 2 (combine n (Names.DirPath.hash d))
end
(* let hcons = Hashcons.simple_hcons Hunivlevel.generate Names.DirPath.hcons *)
@@ -1898,7 +1904,7 @@ let check_context_subset (univs, cst) (univs', cst') =
(** Substitutions. *)
let make_universe_subst inst (ctx, csts) =
- try Array.fold_left2 (fun acc c i -> LMap.add c (Universe.make i) acc)
+ try Array.fold_left2 (fun acc c i -> LMap.add c i acc)
LMap.empty (Instance.to_array ctx) (Instance.to_array inst)
with Invalid_argument _ ->
anomaly (Pp.str "Mismatched instance and context when building universe substitution")
@@ -2115,7 +2121,7 @@ let subst_univs_universe_constraints subst csts =
(** Substitute instance inst for ctx in csts *)
let instantiate_univ_context subst (_, csts) =
- subst_univs_constraints (make_subst subst) csts
+ subst_univs_level_constraints subst csts
let check_consistent_constraints (ctx,cstrs) cstrs' =
(* TODO *) ()
diff --git a/kernel/univ.mli b/kernel/univ.mli
index cc5eedefb..bf04c62e2 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -355,15 +355,13 @@ val constraints_of : 'a constrained -> constraints
val check_context_subset : universe_context_set -> universe_context -> universe_context
(** Make a universe level substitution: the list must match the context variables. *)
-val make_universe_subst : Instance.t -> universe_context -> universe_subst
-val empty_subst : universe_subst
-val is_empty_subst : universe_subst -> bool
+val make_universe_subst : Instance.t -> universe_context -> universe_level_subst
val empty_level_subst : universe_level_subst
val is_empty_level_subst : universe_level_subst -> bool
(** Get the instantiated graph. *)
-val instantiate_univ_context : universe_subst -> universe_context -> constraints
+val instantiate_univ_context : universe_level_subst -> universe_context -> constraints
(** Substitution of universes. *)
val subst_univs_level_level : universe_level_subst -> universe_level -> universe_level
@@ -372,6 +370,9 @@ val subst_univs_level_constraints : universe_level_subst -> constraints -> const
val normalize_univs_level_level : universe_level_subst -> universe_level -> universe_level
+
+val empty_subst : universe_subst
+val is_empty_subst : universe_subst -> bool
val make_subst : universe_subst -> universe_subst_fn
(* val subst_univs_level_fail : universe_subst_fn -> universe_level -> universe_level *)
diff --git a/kernel/vars.ml b/kernel/vars.ml
index 40a797a90..120c07d30 100644
--- a/kernel/vars.ml
+++ b/kernel/vars.ml
@@ -299,5 +299,5 @@ let subst_univs_level_constr subst c =
let c' = aux c in
if !changed then c' else c
-let subst_univs_context s =
- map_rel_context (subst_univs_constr s)
+let subst_univs_level_context s =
+ map_rel_context (subst_univs_level_constr s)
diff --git a/kernel/vars.mli b/kernel/vars.mli
index 9d5d16d0c..b4f616b13 100644
--- a/kernel/vars.mli
+++ b/kernel/vars.mli
@@ -78,7 +78,9 @@ val subst_univs_fn_puniverses : universe_level_subst_fn ->
'a puniverses -> 'a puniverses
val subst_univs_constr : universe_subst -> constr -> constr
+
+(** Level substitutions for polymorphism. *)
+
val subst_univs_puniverses : universe_level_subst -> 'a puniverses -> 'a puniverses
val subst_univs_level_constr : universe_level_subst -> constr -> constr
-
-val subst_univs_context : Univ.universe_subst -> rel_context -> rel_context
+val subst_univs_level_context : Univ.universe_level_subst -> rel_context -> rel_context
diff --git a/library/universes.ml b/library/universes.ml
index dd5331fa7..f6922e495 100644
--- a/library/universes.ml
+++ b/library/universes.ml
@@ -41,43 +41,56 @@ let fresh_instance_from_context ctx =
(inst, subst), constraints
let fresh_instance ctx =
- let s = ref LSet.empty in
+ let ctx' = ref LSet.empty in
+ let s = ref LMap.empty in
let inst =
- Instance.subst_fn (fun _ ->
- let u = new_univ_level (Global.current_dirpath ()) in
- s := LSet.add u !s; u)
+ Instance.subst_fn (fun v ->
+ let u = new_univ_level (Global.current_dirpath ()) in
+ ctx' := LSet.add u !ctx';
+ s := LMap.add v u !s; u)
(UContext.instance ctx)
- in !s, inst
-
-let fresh_instance_from ctx =
- let ctx', inst = fresh_instance ctx in
- let subst = make_universe_subst inst ctx in
+ in !ctx', !s, inst
+
+let existing_instance ctx inst =
+ let s = ref LMap.empty in
+ let () =
+ Array.iter2 (fun u v ->
+ s := LMap.add v u !s)
+ (Instance.to_array inst) (Instance.to_array (UContext.instance ctx))
+ in LSet.empty, !s, inst
+
+let fresh_instance_from ctx inst =
+ let ctx', subst, inst =
+ match inst with
+ | Some inst -> existing_instance ctx inst
+ | None -> fresh_instance ctx
+ in
let constraints = instantiate_univ_context subst ctx in
(inst, subst), (ctx', constraints)
-
+
let unsafe_instance_from ctx =
(Univ.UContext.instance ctx, ctx)
-
+
(** Fresh universe polymorphic construction *)
-let fresh_constant_instance env c =
+let fresh_constant_instance env c inst =
let cb = lookup_constant c env in
if cb.Declarations.const_polymorphic then
- let (inst,_), ctx = fresh_instance_from (Declareops.universes_of_constant cb) in
+ let (inst,_), ctx = fresh_instance_from (Declareops.universes_of_constant cb) inst in
((c, inst), ctx)
else ((c,Instance.empty), ContextSet.empty)
-let fresh_inductive_instance env ind =
+let fresh_inductive_instance env ind inst =
let mib, mip = Inductive.lookup_mind_specif env ind in
if mib.Declarations.mind_polymorphic then
- let (inst,_), ctx = fresh_instance_from mib.Declarations.mind_universes in
+ let (inst,_), ctx = fresh_instance_from mib.Declarations.mind_universes inst in
((ind,inst), ctx)
else ((ind,Instance.empty), ContextSet.empty)
-let fresh_constructor_instance env (ind,i) =
+let fresh_constructor_instance env (ind,i) inst =
let mib, mip = Inductive.lookup_mind_specif env ind in
if mib.Declarations.mind_polymorphic then
- let (inst,_), ctx = fresh_instance_from mib.Declarations.mind_universes in
+ let (inst,_), ctx = fresh_instance_from mib.Declarations.mind_universes inst in
(((ind,i),inst), ctx)
else (((ind,i),Instance.empty), ContextSet.empty)
@@ -104,19 +117,28 @@ let unsafe_constructor_instance env (ind,i) =
open Globnames
-let fresh_global_instance env gr =
+let fresh_global_instance ?names env gr =
match gr with
| VarRef id -> mkVar id, ContextSet.empty
| ConstRef sp ->
- let c, ctx = fresh_constant_instance env sp in
+ let c, ctx = fresh_constant_instance env sp names in
mkConstU c, ctx
| ConstructRef sp ->
- let c, ctx = fresh_constructor_instance env sp in
+ let c, ctx = fresh_constructor_instance env sp names in
mkConstructU c, ctx
| IndRef sp ->
- let c, ctx = fresh_inductive_instance env sp in
+ let c, ctx = fresh_inductive_instance env sp names in
mkIndU c, ctx
+let fresh_constant_instance env sp =
+ fresh_constant_instance env sp None
+
+let fresh_inductive_instance env sp =
+ fresh_inductive_instance env sp None
+
+let fresh_constructor_instance env sp =
+ fresh_constructor_instance env sp None
+
let unsafe_global_instance env gr =
match gr with
| VarRef id -> mkVar id, UContext.empty
@@ -185,14 +207,15 @@ let type_of_reference env r =
let cb = Environ.lookup_constant c env in
let ty = Typeops.type_of_constant_type env cb.const_type in
if cb.const_polymorphic then
- let (inst, subst), ctx = fresh_instance_from (Declareops.universes_of_constant cb) in
- Vars.subst_univs_constr subst ty, ctx
+ let (inst, subst), ctx =
+ fresh_instance_from (Declareops.universes_of_constant cb) None in
+ Vars.subst_univs_level_constr subst ty, ctx
else ty, ContextSet.empty
| IndRef ind ->
let (mib, oib as specif) = Inductive.lookup_mind_specif env ind in
if mib.mind_polymorphic then
- let (inst, subst), ctx = fresh_instance_from mib.mind_universes in
+ let (inst, subst), ctx = fresh_instance_from mib.mind_universes None in
let ty = Inductive.type_of_inductive env (specif, inst) in
ty, ctx
else
@@ -201,7 +224,7 @@ let type_of_reference env r =
| ConstructRef cstr ->
let (mib,oib as specif) = Inductive.lookup_mind_specif env (inductive_of_constructor cstr) in
if mib.mind_polymorphic then
- let (inst, subst), ctx = fresh_instance_from mib.mind_universes in
+ let (inst, subst), ctx = fresh_instance_from mib.mind_universes None in
Inductive.type_of_constructor (cstr,inst) specif, ctx
else Inductive.type_of_constructor (cstr,Instance.empty) specif, ContextSet.empty
diff --git a/library/universes.mli b/library/universes.mli
index 4544bd4d3..e5d3ded58 100644
--- a/library/universes.mli
+++ b/library/universes.mli
@@ -26,24 +26,24 @@ val new_Type_sort : Names.dir_path -> sorts
the instantiated constraints. *)
val fresh_instance_from_context : universe_context ->
- (universe_instance * universe_subst) constrained
+ (universe_instance * universe_level_subst) constrained
-val fresh_instance_from : universe_context ->
- (universe_instance * universe_subst) in_universe_context_set
+val fresh_instance_from : universe_context -> universe_instance option ->
+ (universe_instance * universe_level_subst) in_universe_context_set
val new_global_univ : unit -> universe in_universe_context_set
val new_sort_in_family : sorts_family -> sorts
val fresh_sort_in_family : env -> sorts_family ->
sorts in_universe_context_set
-val fresh_constant_instance : env -> constant ->
+val fresh_constant_instance : env -> constant ->
pconstant in_universe_context_set
-val fresh_inductive_instance : env -> inductive ->
+val fresh_inductive_instance : env -> inductive ->
pinductive in_universe_context_set
-val fresh_constructor_instance : env -> constructor ->
+val fresh_constructor_instance : env -> constructor ->
pconstructor in_universe_context_set
-val fresh_global_instance : env -> Globnames.global_reference ->
+val fresh_global_instance : ?names:Univ.Instance.t -> env -> Globnames.global_reference ->
constr in_universe_context_set
val fresh_global_or_constr_instance : env -> Globnames.global_reference_or_constr ->
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index 499e7b053..81645a580 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -152,7 +152,9 @@ GEXTEND Gram
sort:
[ [ "Set" -> GSet
| "Prop" -> GProp
- | "Type" -> GType None ] ]
+ | "Type" -> GType None
+ | "Type"; "{"; id = string; "}" -> GType (Some id)
+ ] ]
;
lconstr:
[ [ c = operconstr LEVEL "200" -> c ] ]
@@ -277,13 +279,17 @@ GEXTEND Gram
| c=operconstr LEVEL "9" -> (c,None) ] ]
;
atomic_constr:
- [ [ g=global -> CRef (g,None)
+ [ [ g=global; i=instance -> CRef (g,i)
| s=sort -> CSort (!@loc,s)
| n=INT -> CPrim (!@loc, Numeral (Bigint.of_string n))
| s=string -> CPrim (!@loc, String s)
| "_" -> CHole (!@loc, None, None)
| id=pattern_ident -> CPatVar(!@loc,(false,id)) ] ]
;
+ instance:
+ [ [ "@{"; l = LIST1 sort SEP ","; "}" -> Some l
+ | -> None ] ]
+ ;
fix_constr:
[ [ fx1=single_fix -> mk_single_fix fx1
| (_,kw,dcl1)=single_fix; "with"; dcls=LIST1 fix_decl SEP "with";
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 652c5acf9..65a8f338c 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -381,9 +381,12 @@ type binder_kind = BProd | BLambda | BLetIn
let detype_anonymous = ref (fun loc n -> anomaly ~label:"detype" (Pp.str "index to an anonymous variable"))
let set_detype_anonymous f = detype_anonymous := f
-let option_of_instance l =
+let detype_level l =
+ GType (Some (Pp.string_of_ppcmds (Univ.Level.pr l)))
+
+let detype_instance l =
if Univ.Instance.is_empty l then None
- else Some l
+ else Some (List.map detype_level (Array.to_list (Univ.Instance.to_array l)))
let rec detype (isgoal:bool) avoid env t =
match kind_of_term (collapse_appl t) with
@@ -424,18 +427,16 @@ let rec detype (isgoal:bool) avoid env t =
in
mkapp (detype isgoal avoid env f)
(Array.map_to_list (detype isgoal avoid env) args)
- (* GApp (dl,detype isgoal avoid env f, *)
- (* Array.map_to_list (detype isgoal avoid env) args) *)
- | Const (sp,u) -> GRef (dl, ConstRef sp, option_of_instance u)
+ | Const (sp,u) -> GRef (dl, ConstRef sp, detype_instance u)
| Proj (p,c) ->
GProj (dl, p, detype isgoal avoid env c)
| Evar (ev,cl) ->
GEvar (dl, ev,
Some (List.map (detype isgoal avoid env) (Array.to_list cl)))
| Ind (ind_sp,u) ->
- GRef (dl, IndRef ind_sp, option_of_instance u)
+ GRef (dl, IndRef ind_sp, detype_instance u)
| Construct (cstr_sp,u) ->
- GRef (dl, ConstructRef cstr_sp, option_of_instance u)
+ GRef (dl, ConstructRef cstr_sp, detype_instance u)
| Case (ci,p,c,bl) ->
let comp = computable p (ci.ci_pp_info.ind_nargs) in
detype_case comp (detype isgoal avoid env)
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index 42d98cdfe..e8b360b86 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -262,9 +262,29 @@ let instantiate_evar_array info c args =
| [] -> c
| _ -> replace_vars inst c
+module StringOrd = struct type t = string let compare = String.compare end
+module UNameMap = struct
+
+ include Map.Make(StringOrd)
+
+ let union s t =
+ merge (fun k l r ->
+ match l, r with
+ | Some _, _ -> l
+ | _, _ -> r) s t
+
+ let diff ext orig =
+ fold (fun u v acc ->
+ if mem u orig then acc
+ else add u v acc)
+ ext empty
+
+end
+
(* 2nd part used to check consistency on the fly. *)
type evar_universe_context =
- { uctx_local : Univ.universe_context_set; (** The local context of variables *)
+ { uctx_names : Univ.Level.t UNameMap.t;
+ uctx_local : Univ.universe_context_set; (** The local context of variables *)
uctx_univ_variables : Universes.universe_opt_subst;
(** The local universes that are unification variables *)
uctx_univ_algebraic : Univ.universe_set;
@@ -277,7 +297,8 @@ type evar_universe_context =
}
let empty_evar_universe_context =
- { uctx_local = Univ.ContextSet.empty;
+ { uctx_names = UNameMap.empty;
+ uctx_local = Univ.ContextSet.empty;
uctx_univ_variables = Univ.LMap.empty;
uctx_univ_algebraic = Univ.LSet.empty;
uctx_univ_template = Univ.LSet.empty;
@@ -301,7 +322,12 @@ let union_evar_universe_context ctx ctx' =
if ctx.uctx_local == ctx'.uctx_local then ctx.uctx_local
else Univ.ContextSet.union ctx.uctx_local ctx'.uctx_local
in
- { uctx_local = local;
+ let names =
+ if ctx.uctx_names = ctx.uctx_names then ctx.uctx_names
+ else UNameMap.union ctx.uctx_names ctx'.uctx_names
+ in
+ { uctx_names = names;
+ uctx_local = local;
uctx_univ_variables =
Univ.LMap.subst_union ctx.uctx_univ_variables ctx'.uctx_univ_variables;
uctx_univ_algebraic =
@@ -323,7 +349,9 @@ let diff_evar_universe_context ctx' ctx =
if ctx == ctx' then empty_evar_universe_context
else
let local = Univ.ContextSet.diff ctx'.uctx_local ctx.uctx_local in
- { uctx_local = local;
+ let names = UNameMap.diff ctx'.uctx_names ctx.uctx_names in
+ { uctx_names = names;
+ uctx_local = local;
uctx_univ_variables =
Univ.LMap.diff ctx'.uctx_univ_variables ctx.uctx_univ_variables;
uctx_univ_algebraic =
@@ -964,7 +992,7 @@ let merge_universe_subst evd subst =
let with_context_set rigid d (a, ctx) =
(merge_context_set rigid d ctx, a)
-let uctx_new_univ_variable template rigid
+let uctx_new_univ_variable template rigid name
({ uctx_local = ctx; uctx_univ_variables = uvars; uctx_univ_algebraic = avars} as uctx) =
let u = Universes.new_univ_level (Global.current_dirpath ()) in
let ctx' = Univ.ContextSet.union ctx (Univ.ContextSet.singleton u) in
@@ -980,14 +1008,23 @@ let uctx_new_univ_variable template rigid
{uctx' with uctx_univ_template = Univ.LSet.add u uctx'.uctx_univ_template}
else uctx'
in
- {uctx'' with uctx_local = ctx'}, u
+ let names =
+ match name with
+ | Some n -> UNameMap.add n u uctx.uctx_names
+ | None -> uctx.uctx_names
+ in
+ {uctx'' with uctx_names = names; uctx_local = ctx'}, u
+
+let new_univ_level_variable ?(template=false) ?name rigid evd =
+ let uctx', u = uctx_new_univ_variable template rigid name evd.universes in
+ ({evd with universes = uctx'}, u)
-let new_univ_variable ?(template=false) rigid evd =
- let uctx', u = uctx_new_univ_variable template rigid evd.universes in
+let new_univ_variable ?(template=false) ?name rigid evd =
+ let uctx', u = uctx_new_univ_variable template rigid name evd.universes in
({evd with universes = uctx'}, Univ.Universe.make u)
-let new_sort_variable ?(template=false) rigid d =
- let (d', u) = new_univ_variable ~template rigid d in
+let new_sort_variable ?(template=false) ?name rigid d =
+ let (d', u) = new_univ_variable ~template rigid ?name d in
(d', Type u)
let make_flexible_variable evd b u =
@@ -1013,7 +1050,7 @@ let make_flexible_variable evd b u =
let fresh_sort_in_family env evd s =
with_context_set univ_flexible evd (Universes.fresh_sort_in_family env s)
-let fresh_constant_instance env evd c =
+let fresh_constant_instance env evd c =
with_context_set univ_flexible evd (Universes.fresh_constant_instance env c)
let fresh_inductive_instance env evd i =
@@ -1022,8 +1059,8 @@ let fresh_inductive_instance env evd i =
let fresh_constructor_instance env evd c =
with_context_set univ_flexible evd (Universes.fresh_constructor_instance env c)
-let fresh_global ?(rigid=univ_flexible) env evd gr =
- with_context_set rigid evd (Universes.fresh_global_instance env gr)
+let fresh_global ?(rigid=univ_flexible) ?names env evd gr =
+ with_context_set rigid evd (Universes.fresh_global_instance ?names env gr)
let whd_sort_variable evd t = t
@@ -1203,7 +1240,8 @@ let refresh_undefined_univ_variables uctx =
(Option.map (Univ.subst_univs_level_universe subst) v) acc)
uctx.uctx_univ_variables Univ.LMap.empty
in
- let uctx' = {uctx_local = ctx';
+ let uctx' = {uctx_names = uctx.uctx_names;
+ uctx_local = ctx';
uctx_univ_variables = vars; uctx_univ_algebraic = alg;
uctx_univ_template = uctx.uctx_univ_template;
uctx_universes = Univ.initial_universes;
@@ -1236,7 +1274,8 @@ let normalize_evar_universe_context uctx =
else
let us', universes = Universes.refresh_constraints uctx.uctx_initial_universes us' in
let uctx' =
- { uctx_local = us';
+ { uctx_names = uctx.uctx_names;
+ uctx_local = us';
uctx_univ_variables = vars';
uctx_univ_algebraic = algs';
uctx_univ_template = uctx.uctx_univ_template;
@@ -1265,6 +1304,14 @@ let nf_constraints =
Profile.profile1 nfconstrkey nf_constraints
else nf_constraints
+let universe_of_name evd s =
+ UNameMap.find s evd.universes.uctx_names
+
+let add_universe_name evd s l =
+ let names = evd.universes.uctx_names in
+ let names' = UNameMap.add s l names in
+ {evd with universes = {evd.universes with uctx_names = names'}}
+
let universes evd = evd.universes.uctx_universes
let constraints evd = evd.universes.uctx_universes
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index a360351b7..8a9753e5b 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -258,8 +258,6 @@ val drop_side_effects : evar_map -> evar_map
Evar maps also keep track of the universe constraints defined at a given
point. This section defines the relevant manipulation functions. *)
-val new_univ_variable : evar_map -> evar_map * Univ.universe
-val new_sort_variable : evar_map -> evar_map * sorts
val is_sort_variable : evar_map -> sorts -> bool
val whd_sort_variable : evar_map -> constr -> constr
val set_leq_sort : evar_map -> sorts -> sorts -> evar_map
@@ -424,6 +422,10 @@ val union_evar_universe_context : evar_universe_context -> evar_universe_context
evar_universe_context
val evar_universe_context_subst : evar_universe_context -> Universes.universe_opt_subst
+(** Raises Not_found if not a name for a universe in this map. *)
+val universe_of_name : evar_map -> string -> Univ.universe_level
+val add_universe_name : evar_map -> string -> Univ.universe_level -> evar_map
+
val universes : evar_map -> Univ.universes
val add_constraints_context : evar_universe_context ->
@@ -436,8 +438,9 @@ val normalize_evar_universe_context_variables : evar_universe_context ->
val normalize_evar_universe_context : evar_universe_context ->
evar_universe_context
-val new_univ_variable : ?template:bool -> rigid -> evar_map -> evar_map * Univ.universe
-val new_sort_variable : ?template:bool -> rigid -> evar_map -> evar_map * sorts
+val new_univ_level_variable : ?template:bool -> ?name:string -> rigid -> evar_map -> evar_map * Univ.universe_level
+val new_univ_variable : ?template:bool -> ?name:string -> rigid -> evar_map -> evar_map * Univ.universe
+val new_sort_variable : ?template:bool -> ?name:string -> rigid -> evar_map -> evar_map * sorts
val make_flexible_variable : evar_map -> bool -> Univ.universe_level -> evar_map
val is_sort_variable : evar_map -> sorts -> (Univ.universe_level * bool) option
(** [is_sort_variable evm s] returns [Some (u, is_rigid)] or [None] if [s] is
@@ -489,7 +492,7 @@ val fresh_constant_instance : env -> evar_map -> constant -> evar_map * pconstan
val fresh_inductive_instance : env -> evar_map -> inductive -> evar_map * pinductive
val fresh_constructor_instance : env -> evar_map -> constructor -> evar_map * pconstructor
-val fresh_global : ?rigid:rigid -> env -> evar_map ->
+val fresh_global : ?rigid:rigid -> ?names:Univ.Instance.t -> env -> evar_map ->
Globnames.global_reference -> evar_map * constr
(********************************************************************
diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml
index bed77e622..9f58b4c80 100644
--- a/pretyping/indrec.ml
+++ b/pretyping/indrec.ml
@@ -60,7 +60,7 @@ let check_privacy_block mib =
let mis_make_case_com dep env sigma (ind, u as pind) (mib,mip as specif) kind =
let usubst = Inductive.make_inductive_subst mib u in
- let lnamespar = Vars.subst_univs_context usubst
+ let lnamespar = Vars.subst_univs_level_context usubst
mib.mind_params_ctxt
in
let () = check_privacy_block mib in
@@ -284,7 +284,7 @@ let mis_make_indrec env sigma listdepkind mib u =
let evdref = ref sigma in
let usubst = Inductive.make_inductive_subst mib u in
let lnonparrec,lnamesparrec =
- context_chop (nparams-nparrec) (Vars.subst_univs_context usubst mib.mind_params_ctxt) in
+ context_chop (nparams-nparrec) (Vars.subst_univs_level_context usubst mib.mind_params_ctxt) in
let nrec = List.length listdepkind in
let depPvec =
Array.make mib.mind_ntypes (None : (bool * constr) option) in
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index 07dacd0cc..43552ef54 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -101,7 +101,7 @@ let mis_nf_constructor_type ((ind,u),mib,mip) j =
let make_Ik k = mkIndU (((fst ind),ntypes-k-1),u) in
if j > nconstr then error "Not enough constructors in the type.";
let univsubst = make_inductive_subst mib u in
- substl (List.init ntypes make_Ik) (subst_univs_constr univsubst specif.(j-1))
+ substl (List.init ntypes make_Ik) (subst_univs_level_constr univsubst specif.(j-1))
(* Arity of constructors excluding parameters and local defs *)
@@ -149,7 +149,7 @@ let constructor_nrealhyps (ind,j) =
let get_full_arity_sign env (ind,u) =
let (mib,mip) = Inductive.lookup_mind_specif env ind in
let subst = Inductive.make_inductive_subst mib u in
- Vars.subst_univs_context subst mip.mind_arity_ctxt
+ Vars.subst_univs_level_context subst mip.mind_arity_ctxt
let nconstructors ind =
let (mib,mip) = Inductive.lookup_mind_specif (Global.env()) ind in
@@ -280,11 +280,11 @@ let get_arity env ((ind,u),params) =
snd (List.chop nnonrecparams mib.mind_params_ctxt)
else
parsign in
- let parsign = Vars.subst_univs_context univsubst parsign in
+ let parsign = Vars.subst_univs_level_context univsubst parsign in
let arproperlength = List.length mip.mind_arity_ctxt - List.length parsign in
let arsign,_ = List.chop arproperlength mip.mind_arity_ctxt in
let subst = instantiate_context parsign params in
- let arsign = Vars.subst_univs_context univsubst arsign in
+ let arsign = Vars.subst_univs_level_context univsubst arsign in
(substl_rel_context subst arsign, Inductive.inductive_sort_family mip)
(* Functions to build standard types related to inductive *)
@@ -499,7 +499,7 @@ let type_of_inductive_knowing_conclusion env sigma ((mib,mip),u) conclty =
match mip.mind_arity with
| RegularArity s ->
let subst = Inductive.make_inductive_subst mib u in
- sigma, subst_univs_constr subst s.mind_user_arity
+ sigma, subst_univs_level_constr subst s.mind_user_arity
| TemplateArity ar ->
let _,scl = Reduction.dest_arity env conclty in
let ctx = List.rev mip.mind_arity_ctxt in
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index add47e5b7..31576391b 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -93,10 +93,20 @@ let ((constr_in : constr -> Dyn.t),
(** Miscellaneous interpretation functions *)
+let interp_universe_name evd = function
+ | None -> new_univ_level_variable univ_rigid evd
+ | Some s ->
+ try let level = Evd.universe_of_name evd s in
+ evd, level
+ with Not_found ->
+ new_univ_level_variable ~name:s univ_rigid evd
+
let interp_sort evd = function
| GProp -> evd, Prop Null
| GSet -> evd, Prop Pos
- | GType _ -> new_sort_variable univ_rigid evd
+ | GType n ->
+ let evd, l = interp_universe_name evd n in
+ evd, Type (Univ.Universe.make l)
let interp_elimination_sort = function
| GProp -> InProp
@@ -260,8 +270,23 @@ let evar_kind_of_term sigma c =
(*************************************************************************)
(* Main pretyping function *)
-(* Check with universe list? *)
-let pretype_global rigid env evd gr us = Evd.fresh_global ~rigid env evd gr
+let interp_universe_level_name evd = function
+ | GProp -> evd, Univ.Level.prop
+ | GSet -> evd, Univ.Level.set
+ | GType s -> interp_universe_name evd s
+
+let pretype_global rigid env evd gr us =
+ let evd, instance =
+ match us with
+ | None -> evd, None
+ | Some l ->
+ let evd, l' = List.fold_left (fun (evd, univs) l ->
+ let evd, l = interp_universe_level_name evd l in
+ (evd, l :: univs)) (evd, []) l
+ in
+ evd, Some (Univ.Instance.of_array (Array.of_list (List.rev l')))
+ in
+ Evd.fresh_global ~rigid ?names:instance env evd gr
let is_template_polymorphic_constructor env c =
match kind_of_term c with
@@ -292,10 +317,17 @@ let pretype_ref loc evdref env ref us =
let ty = Retyping.get_type_of env evd c in
make_judge c ty
+let judge_of_Type evd s =
+ let judge s =
+ { uj_val = mkSort (Type s); uj_type = mkSort (Type (Univ.super s)) }
+ in
+ let evd, l = interp_universe_name evd s in
+ evd, judge (Univ.Universe.make l)
+
let pretype_sort evdref = function
| GProp -> judge_of_prop
| GSet -> judge_of_set
- | GType _ -> evd_comb0 judge_of_new_Type evdref
+ | GType s -> evd_comb1 judge_of_Type evdref s
let new_type_evar evdref env loc =
let e, s =
@@ -500,7 +532,7 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref lvar t =
j', (ind, args))
in
let usubst = make_inductive_subst (fst (lookup_mind_specif env ind)) u in
- let ty = Vars.subst_univs_constr usubst ty in
+ let ty = Vars.subst_univs_level_constr usubst ty in
let ty = substl (recty.uj_val :: List.rev pars) ty in
let j = {uj_val = mkProj (cst,recty.uj_val); uj_type = ty} in
inh_conv_coerce_to_tycon loc env evdref j tycon
diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml
index 2cf730f11..b21f4e383 100644
--- a/pretyping/vnorm.ml
+++ b/pretyping/vnorm.ml
@@ -59,7 +59,7 @@ let type_constructor mind mib u typ params =
let s = ind_subst mind mib u in
let ctyp = substl s typ in
let usubst = make_inductive_subst mib u in
- let ctyp = subst_univs_constr usubst ctyp in
+ let ctyp = subst_univs_level_constr usubst ctyp in
let nparams = Array.length params in
if Int.equal nparams 0 then ctyp
else
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index 950594397..019fad0ce 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -119,7 +119,7 @@ let pr_qualid = pr_qualid
let pr_patvar = pr_id
let pr_universe_instance l =
- pr_opt (pr_in_comment Univ.Instance.pr) l
+ pr_opt (pr_in_comment (prlist_with_sep spc pr_glob_sort)) l
let pr_cref ref us =
pr_reference ref ++ pr_universe_instance us
diff --git a/tactics/eqschemes.ml b/tactics/eqschemes.ml
index 08c887b77..7a536b35a 100644
--- a/tactics/eqschemes.ml
+++ b/tactics/eqschemes.ml
@@ -103,7 +103,7 @@ let get_sym_eq_data env (ind,u) =
not (Int.equal (Array.length mip.mind_nf_lc) 1) then
error "Not an inductive type with a single constructor.";
let subst = Inductive.make_inductive_subst mib u in
- let arityctxt = Vars.subst_univs_context subst mip.mind_arity_ctxt in
+ let arityctxt = Vars.subst_univs_level_context subst mip.mind_arity_ctxt in
let realsign,_ = List.chop mip.mind_nrealargs_ctxt arityctxt in
if List.exists (fun (_,b,_) -> not (Option.is_empty b)) realsign then
error "Inductive equalities with local definitions in arity not supported.";
@@ -115,7 +115,7 @@ let get_sym_eq_data env (ind,u) =
if mip.mind_nrealargs > mib.mind_nparams then
error "Constructors arguments must repeat the parameters.";
let _,params2 = List.chop (mib.mind_nparams-mip.mind_nrealargs) params in
- let paramsctxt = Vars.subst_univs_context subst mib.mind_params_ctxt in
+ let paramsctxt = Vars.subst_univs_level_context subst mib.mind_params_ctxt in
let paramsctxt1,_ =
List.chop (mib.mind_nparams-mip.mind_nrealargs) paramsctxt in
if not (List.equal eq_constr params2 constrargs) then
@@ -139,7 +139,7 @@ let get_non_sym_eq_data env (ind,u) =
not (Int.equal (Array.length mip.mind_nf_lc) 1) then
error "Not an inductive type with a single constructor.";
let subst = Inductive.make_inductive_subst mib u in
- let arityctxt = Vars.subst_univs_context subst mip.mind_arity_ctxt in
+ let arityctxt = Vars.subst_univs_level_context subst mip.mind_arity_ctxt in
let realsign,_ = List.chop mip.mind_nrealargs_ctxt arityctxt in
if List.exists (fun (_,b,_) -> not (Option.is_empty b)) realsign then
error "Inductive equalities with local definitions in arity not supported";
@@ -148,8 +148,8 @@ let get_non_sym_eq_data env (ind,u) =
if not (Int.equal (rel_context_length constrsign) (rel_context_length mib.mind_params_ctxt)) then
error "Constructor must have no arguments";
let _,constrargs = List.chop mib.mind_nparams constrargs in
- let constrargs = List.map (Vars.subst_univs_constr subst) constrargs in
- let paramsctxt = Vars.subst_univs_context subst mib.mind_params_ctxt in
+ let constrargs = List.map (Vars.subst_univs_level_constr subst) constrargs in
+ let paramsctxt = Vars.subst_univs_level_context subst mib.mind_params_ctxt in
(specif,constrargs,realsign,paramsctxt,mip.mind_nrealargs)
(**********************************************************************)
@@ -735,8 +735,8 @@ let build_congr env (eq,refl,ctx) ind =
if not (Int.equal mip.mind_nrealargs 1) then
error "Expect an inductive type with one predicate parameter.";
let i = 1 in
- let arityctxt = Vars.subst_univs_context subst mip.mind_arity_ctxt in
- let paramsctxt = Vars.subst_univs_context subst mib.mind_params_ctxt in
+ let arityctxt = Vars.subst_univs_level_context subst mip.mind_arity_ctxt in
+ let paramsctxt = Vars.subst_univs_level_context subst mib.mind_params_ctxt in
let realsign,_ = List.chop mip.mind_nrealargs_ctxt arityctxt in
if List.exists (fun (_,b,_) -> not (Option.is_empty b)) realsign then
error "Inductive equalities with local definitions in arity not supported.";
diff --git a/test-suite/success/polymorphism.v b/test-suite/success/polymorphism.v
index 99284eb54..fd299b43a 100644
--- a/test-suite/success/polymorphism.v
+++ b/test-suite/success/polymorphism.v
@@ -1,3 +1,28 @@
+Module withoutpoly.
+
+Inductive empty :=.
+
+Inductive emptyt : Type :=.
+Inductive singleton : Type :=
+ single.
+Inductive singletoninfo : Type :=
+ singleinfo : unit -> singletoninfo.
+Inductive singletonset : Set :=
+ singleset.
+
+Inductive singletonnoninfo : Type :=
+ singlenoninfo : empty -> singletonnoninfo.
+
+Inductive singletoninfononinfo : Prop :=
+ singleinfononinfo : unit -> singletoninfononinfo.
+
+Inductive bool : Type :=
+ | true | false.
+
+Inductive smashedbool : Prop :=
+ | trueP | falseP.
+End withoutpoly.
+
Set Universe Polymorphism.
Inductive empty :=.
@@ -225,7 +250,7 @@ Fail Check fun A : Type => foo A.
Check fun A : Prop => foo A.
Fail Definition bar := fun A : Set => foo A.
-Fail Check (let A := Type in foo (id A)).
+Check (let A := Type in foo (id A)).
Definition fooS (A : Set) := A.
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-06 13:15:07 +0000