aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--grammar/q_constr.ml42
-rw-r--r--interp/constrextern.ml4
-rw-r--r--interp/constrintern.ml4
-rw-r--r--interp/notation_ops.ml2
-rw-r--r--intf/constrexpr.mli2
-rw-r--r--intf/glob_term.mli2
-rw-r--r--intf/misctypes.mli8
-rw-r--r--parsing/g_constr.ml49
-rw-r--r--plugins/funind/glob_term_to_relation.ml2
-rw-r--r--plugins/funind/invfun.ml2
-rw-r--r--pretyping/detyping.ml6
-rw-r--r--pretyping/miscops.ml3
-rw-r--r--pretyping/patternops.ml2
-rw-r--r--pretyping/pretyping.ml47
-rw-r--r--printing/ppconstr.ml8
-rw-r--r--test-suite/success/namedunivs.v4
-rw-r--r--toplevel/command.ml4
17 files changed, 68 insertions, 43 deletions
diff --git a/grammar/q_constr.ml4 b/grammar/q_constr.ml4
index cf671adcb2..e1db0a05a3 100644
--- a/grammar/q_constr.ml4
+++ b/grammar/q_constr.ml4
@@ -30,7 +30,7 @@ EXTEND
sort:
[ [ "Set" -> Misctypes.GSet
| "Prop" -> Misctypes.GProp
- | "Type" -> Misctypes.GType None ] ]
+ | "Type" -> Misctypes.GType [] ] ]
;
ident:
[ [ s = string -> <:expr< Names.Id.of_string $str:s$ >> ] ]
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 36fa81157a..d51d067b28 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -595,8 +595,8 @@ let extern_optimal_prim_token scopes r r' =
let extern_glob_sort = function
| GProp -> GProp
| GSet -> GSet
- | GType (Some _) as s when !print_universes -> s
- | GType _ -> GType None
+ | GType _ as s when !print_universes -> s
+ | GType _ -> GType []
let extern_universes = function
| Some _ as l when !print_universes -> l
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 8f76bbb61b..7db2203c08 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -1360,7 +1360,9 @@ 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 us [] 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) ->
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index 5cad2b54d6..9461cebb0f 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -731,7 +731,7 @@ let rec match_ inner u alp (tmetas,blmetas as metas) sigma a1 a2 =
match_in u alp metas (match_in u alp metas sigma c1 c2) t1 t2
| GCast(_,c1, CastCoerce), NCast(c2, CastCoerce) ->
match_in u alp metas sigma c1 c2
- | GSort (_,GType _), NSort (GType None) when not u -> sigma
+ | GSort (_,GType _), NSort (GType _) when not u -> sigma
| GSort (_,s1), NSort s2 when Miscops.glob_sort_eq s1 s2 -> sigma
| GPatVar _, NHole _ -> (*Don't hide Metas, they bind in ltac*) raise No_match
| a, NHole _ -> sigma
diff --git a/intf/constrexpr.mli b/intf/constrexpr.mli
index c28c4dcb18..eb39a9bde6 100644
--- a/intf/constrexpr.mli
+++ b/intf/constrexpr.mli
@@ -61,7 +61,7 @@ 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 instance_expr = Misctypes.glob_level list
type constr_expr =
| CRef of reference * instance_expr option
diff --git a/intf/glob_term.mli b/intf/glob_term.mli
index b4543bb59b..d0b6939e24 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 * glob_sort list option)
+ | GRef of (Loc.t * global_reference * glob_level 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/intf/misctypes.mli b/intf/misctypes.mli
index 390711fabd..c61da0e306 100644
--- a/intf/misctypes.mli
+++ b/intf/misctypes.mli
@@ -43,8 +43,12 @@ type 'id move_location =
(** Sorts *)
-type sort_info = string option
-type glob_sort = GProp | GSet | GType of sort_info
+type 'a glob_sort_gen = GProp | GSet | GType of 'a
+type sort_info = string list
+type level_info = string option
+
+type glob_sort = sort_info glob_sort_gen
+type glob_level = level_info glob_sort_gen
(** A synonym of [Evar.t], also defined in Term *)
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index be343b9873..272a18c3e1 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -152,8 +152,13 @@ GEXTEND Gram
sort:
[ [ "Set" -> GSet
| "Prop" -> GProp
- | "Type" -> GType None
- | "Type"; "@{"; id = ident; "}" -> GType (Some (Id.to_string id))
+ | "Type" -> GType []
+ | "Type"; "@{"; u = universe; "}" -> GType (List.map Id.to_string u)
+ ] ]
+ ;
+ universe:
+ [ [ "max("; ids = LIST1 ident SEP ","; ")" -> ids
+ | id = ident -> [id]
] ]
;
lconstr:
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index 2ef3c34ed7..587af35acb 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -1229,7 +1229,7 @@ let rec rebuild_return_type rt =
Constrexpr.CLetIn(loc,na,t,rebuild_return_type t')
| _ -> Constrexpr.CProdN(Loc.ghost,[[Loc.ghost,Anonymous],
Constrexpr.Default Decl_kinds.Explicit,rt],
- Constrexpr.CSort(Loc.ghost,GType None))
+ Constrexpr.CSort(Loc.ghost,GType []))
let do_build_inductive
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index 97157facd0..832e933a71 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -1064,7 +1064,7 @@ let derive_correctness make_scheme functional_induction (funs: constant list) (g
(fun entry ->
(fst (fst(Future.force entry.Entries.const_entry_body)), Option.get entry.Entries.const_entry_type )
)
- (make_scheme (Array.map_to_list (fun const -> const,GType None) funs))
+ (make_scheme (Array.map_to_list (fun const -> const,GType []) funs))
)
in
let proving_tac =
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index bdec8307a1..3a355b91a9 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -374,9 +374,9 @@ let detype_sort = function
let _, map = Universes.global_universe_names () in
let pr_level u =
try Nameops.pr_id (Univ.LMap.find u map) with Not_found -> Univ.Level.pr u
- in
- Some (Pp.string_of_ppcmds (Univ.Universe.pr_with pr_level u))
- else None)
+ in
+ [Pp.string_of_ppcmds (Univ.Universe.pr_with pr_level u)]
+ else [])
type binder_kind = BProd | BLambda | BLetIn
diff --git a/pretyping/miscops.ml b/pretyping/miscops.ml
index ab01065b19..5b5bbe095b 100644
--- a/pretyping/miscops.ml
+++ b/pretyping/miscops.ml
@@ -28,6 +28,5 @@ let smartmap_cast_type f c =
let glob_sort_eq g1 g2 = match g1, g2 with
| GProp, GProp -> true
| GSet, GSet -> true
-| GType None, GType None -> true
-| GType (Some s1), GType (Some s2) -> CString.equal s1 s2
+| GType l1, GType l2 -> List.for_all2 CString.equal l1 l2
| _ -> false
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index 8557953cc4..5828e7f433 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -129,7 +129,7 @@ let pattern_of_constr sigma t =
| Var id -> PVar id
| Sort (Prop Null) -> PSort GProp
| Sort (Prop Pos) -> PSort GSet
- | Sort (Type _) -> PSort (GType None)
+ | Sort (Type _) -> PSort (GType [])
| Cast (c,_,_) -> pattern_of_constr c
| LetIn (na,c,_,b) -> PLetIn (na,pattern_of_constr c,pattern_of_constr b)
| Prod (na,c,b) -> PProd (na,pattern_of_constr c,pattern_of_constr b)
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index c6a4703a08..6d98602b51 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -98,26 +98,36 @@ let ((constr_in : constr -> Dyn.t),
(constr_out : Dyn.t -> constr)) = Dyn.create "constr"
(** Miscellaneous interpretation functions *)
-
-let interp_universe_name evd = function
+let interp_universe_level_name evd s =
+ let names, _ = Universes.global_universe_names () in
+ try
+ let id = try Id.of_string s with _ -> raise Not_found in
+ evd, Idmap.find id names
+ with Not_found ->
+ 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_universe evd = function
+ | [] -> let evd, l = new_univ_level_variable univ_rigid evd in
+ evd, Univ.Universe.make l
+ | l ->
+ List.fold_left (fun (evd, u) l ->
+ let evd', l = interp_universe_level_name evd l in
+ (evd', Univ.sup u (Univ.Universe.make l)))
+ (evd, Univ.Universe.type0m) l
+
+let interp_universe_level evd = function
| None -> new_univ_level_variable univ_rigid evd
- | Some s ->
- try
- let id = try Id.of_string s with _ -> raise Not_found in
- let names, _ = Universes.global_universe_names () in
- evd, Idmap.find id names
- with Not_found ->
- try let level = Evd.universe_of_name evd s in
- evd, level
- with Not_found ->
- new_univ_level_variable ~name:s univ_rigid evd
-
+ | Some s -> interp_universe_level_name evd s
+
let interp_sort evd = function
| GProp -> evd, Prop Null
| GSet -> evd, Prop Pos
| GType n ->
- let evd, l = interp_universe_name evd n in
- evd, Type (Univ.Universe.make l)
+ let evd, u = interp_universe evd n in
+ evd, Type u
let interp_elimination_sort = function
| GProp -> InProp
@@ -303,7 +313,7 @@ let evar_kind_of_term sigma c =
let interp_universe_level_name evd = function
| GProp -> evd, Univ.Level.prop
| GSet -> evd, Univ.Level.set
- | GType s -> interp_universe_name evd s
+ | GType s -> interp_universe_level evd s
let pretype_global loc rigid env evd gr us =
let evd, instance =
@@ -330,8 +340,6 @@ let pretype_ref loc evdref env ref us =
| VarRef id ->
(* Section variable *)
(try let (_,_,ty) = lookup_named id env in
- (* let ctx = Decls.variable_context id in *)
- (* evdref := Evd.merge_context_set univ_rigid !evdref ctx; *)
make_judge (mkVar id) ty
with Not_found ->
(* This may happen if env is a goal env and section variables have
@@ -345,8 +353,7 @@ let pretype_ref loc evdref env ref us =
make_judge c ty
let judge_of_Type evd s =
- let evd, l = interp_universe_name evd s in
- let s = Univ.Universe.make l in
+ let evd, s = interp_universe evd s in
let judge =
{ uj_val = mkSort (Type s); uj_type = mkSort (Type (Univ.super s)) }
in
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index fb40e90d36..0fb97ad16e 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -108,12 +108,18 @@ let pr_sep_com sep f c = pr_with_comments (constr_loc c) (sep() ++ f c)
let pr_in_comment pr x = str "(* " ++ pr x ++ str " *)"
+let pr_univ l =
+ match l with
+ | [x] -> str x
+ | l -> str"max(" ++ prlist_with_sep (fun () -> str",") str l ++ str")"
+
let pr_univ_annot pr x = str "@{" ++ pr x ++ str "}"
let pr_glob_sort = function
| GProp -> str "Prop"
| GSet -> str "Set"
- | GType u -> hov 0 (str "Type" ++ pr_opt_no_spc (pr_univ_annot str) u)
+ | GType [] -> str "Type"
+ | GType u -> hov 0 (str "Type" ++ pr_univ_annot pr_univ u)
let pr_id = pr_id
let pr_name = pr_name
diff --git a/test-suite/success/namedunivs.v b/test-suite/success/namedunivs.v
index 5c0a3c7f23..059462fac3 100644
--- a/test-suite/success/namedunivs.v
+++ b/test-suite/success/namedunivs.v
@@ -30,6 +30,9 @@ Definition foo' {A : Type@{i}} (o : option@{i} A) : option@{i} A :=
Definition foo'' {A : Type@{i}} (o : option@{j} A) : option@{k} A :=
o.
+
+Definition testm (A : Type@{i}) : Type@{max(i,j)} := A.
+
(* Inductive prod (A : Type@{i}) (B : Type@{j}) := *)
(* | pair : A -> B -> prod A B. *)
@@ -43,7 +46,6 @@ Definition foo'' {A : Type@{i}} (o : option@{j} A) : option@{k} A :=
(* | pair _ _ a b => b *)
(* end. *)
-
(* Inductive paths {A : Type} : A -> A -> Type := *)
(* | idpath (a : A) : paths a a. *)
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 582dde30d3..9b650f859a 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -333,7 +333,7 @@ let prepare_param = function
let rec check_anonymous_type ind =
let open Glob_term in
match ind with
- | GSort (_, GType None) -> true
+ | GSort (_, GType []) -> true
| GProd (_, _, _, _, e)
| GLetIn (_, _, _, e)
| GLambda (_, _, _, _, e)
@@ -570,7 +570,7 @@ let extract_params indl =
let extract_inductive indl =
List.map (fun ((_,indname),_,ar,lc) -> {
ind_name = indname;
- ind_arity = Option.cata (fun x -> x) (CSort (Loc.ghost,GType None)) ar;
+ ind_arity = Option.cata (fun x -> x) (CSort (Loc.ghost,GType [])) ar;
ind_lc = List.map (fun (_,((_,id),t)) -> (id,t)) lc
}) indl
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 16:23:02 +0000