aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--interp/constrextern.ml10
-rw-r--r--interp/constrintern.ml12
-rw-r--r--parsing/g_constr.mlg14
-rw-r--r--plugins/funind/glob_term_to_relation.ml2
-rw-r--r--plugins/ssr/ssrcommon.ml4
-rw-r--r--pretyping/detyping.ml6
-rw-r--r--pretyping/glob_ops.ml21
-rw-r--r--pretyping/glob_term.ml10
-rw-r--r--pretyping/pretyping.ml27
-rw-r--r--printing/ppconstr.ml11
-rw-r--r--vernac/comInductive.ml4
-rw-r--r--vernac/record.ml2
12 files changed, 63 insertions, 60 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index fe50bd4b08..c05af8be45 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -757,11 +757,9 @@ let extended_glob_local_binder_of_decl ?loc u = DAst.make ?loc (extended_glob_lo
(* mapping glob_constr to constr_expr *)
let extern_glob_sort = function
- | GSProp -> GSProp
- | GProp -> GProp
- | GSet -> GSet
- | GType _ as s when !print_universes -> s
- | GType _ -> GType []
+ (* In case we print a glob_constr w/o having passed through detyping *)
+ | GType _ when not !print_universes -> GType UUnknown
+ | u -> u
let extern_universes = function
| Some _ as l when !print_universes -> l
@@ -1315,7 +1313,7 @@ let rec glob_of_pat avoid env sigma pat = DAst.make @@ match pat with
| PSort Sorts.InSProp -> GSort GSProp
| PSort Sorts.InProp -> GSort GProp
| PSort Sorts.InSet -> GSort GSet
- | PSort Sorts.InType -> GSort (GType [])
+ | PSort Sorts.InType -> GSort (GType UUnknown)
| PInt i -> GInt i
let extern_constr_pattern env sigma pat =
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 1dd68f2abf..b4294b4ff8 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -998,18 +998,18 @@ let intern_reference qid =
in
Smartlocate.global_of_extended_global r
-let sort_info_of_level_info (info: level_info) : (Libnames.qualid * int) option =
+let sort_info_of_level_info (info: level_info) : sort_info =
match info with
- | UAnonymous -> None
- | UUnknown -> None
- | UNamed id -> Some (id, 0)
+ | UAnonymous -> UAnonymous
+ | UUnknown -> UUnknown
+ | UNamed id -> UNamed [id,0]
let glob_sort_of_level (level: glob_level) : glob_sort =
match level with
| GSProp -> GSProp
| GProp -> GProp
| GSet -> GSet
- | GType info -> GType [sort_info_of_level_info info]
+ | GType info -> GType (sort_info_of_level_info info)
(* Is it a global reference or a syntactic definition? *)
let intern_qualid ?(no_secvar=false) qid intern env ntnvars us args =
@@ -1045,7 +1045,7 @@ let intern_qualid ?(no_secvar=false) qid intern env ntnvars us args =
DAst.make ?loc @@ GApp (DAst.make ?loc:loc' @@ GRef (ref, us), arg)
| _ -> err ()
end
- | Some [s], GSort (GType []) -> DAst.make ?loc @@ GSort (glob_sort_of_level s)
+ | Some [s], GSort (GType UUnknown) -> DAst.make ?loc @@ GSort (glob_sort_of_level s)
| Some [_old_level], GSort _new_sort ->
(* TODO: add old_level and new_sort to the error message *)
user_err ?loc (str "Cannot change universe level of notation " ++ pr_qualid qid)
diff --git a/parsing/g_constr.mlg b/parsing/g_constr.mlg
index bd88570224..dd68b411a0 100644
--- a/parsing/g_constr.mlg
+++ b/parsing/g_constr.mlg
@@ -156,7 +156,7 @@ GRAMMAR EXTEND Gram
[ [ "Set" -> { GSet }
| "Prop" -> { GProp }
| "SProp" -> { GSProp }
- | "Type" -> { GType [] }
+ | "Type" -> { GType UUnknown }
| "Type"; "@{"; u = universe; "}" -> { GType u }
] ]
;
@@ -168,14 +168,14 @@ GRAMMAR EXTEND Gram
] ]
;
universe_expr:
- [ [ id = global; "+"; n = natural -> { Some (id,n) }
- | id = global -> { Some (id,0) }
- | "_" -> { None }
- ] ]
+ [ [ id = global; "+"; n = natural -> { (id,n) }
+ | id = global -> { (id,0) }
+ ] ]
;
universe:
- [ [ IDENT "max"; "("; ids = LIST1 universe_expr SEP ","; ")" -> { ids }
- | u = universe_expr -> { [u] }
+ [ [ IDENT "max"; "("; ids = LIST1 universe_expr SEP ","; ")" -> { UNamed ids }
+ | u = universe_expr -> { UNamed [u] }
+ | "_" -> { UAnonymous }
] ]
;
lconstr:
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index 4c67d65816..889a2d7359 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -1302,7 +1302,7 @@ let rec rebuild_return_type rt =
CAst.make ?loc @@ Constrexpr.CLetIn(na,v,t,rebuild_return_type t')
| _ -> CAst.make ?loc @@ Constrexpr.CProdN([Constrexpr.CLocalAssum ([CAst.make Anonymous],
Constrexpr.Default Decl_kinds.Explicit, rt)],
- CAst.make @@ Constrexpr.CSort(GType []))
+ CAst.make @@ Constrexpr.CSort(GType UUnknown))
let do_build_inductive
evd (funconstants: pconstant list) (funsargs: (Name.t * glob_constr * glob_constr option) list list)
diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml
index 56f17703ff..4470c36888 100644
--- a/plugins/ssr/ssrcommon.ml
+++ b/plugins/ssr/ssrcommon.ml
@@ -194,7 +194,7 @@ let mkRApp f args = if args = [] then f else DAst.make @@ GApp (f, args)
let mkRVar id = DAst.make @@ GRef (VarRef id,None)
let mkRltacVar id = DAst.make @@ GVar (id)
let mkRCast rc rt = DAst.make @@ GCast (rc, CastConv rt)
-let mkRType = DAst.make @@ GSort (GType [])
+let mkRType = DAst.make @@ GSort (GType UUnknown)
let mkRProp = DAst.make @@ GSort (GProp)
let mkRArrow rt1 rt2 = DAst.make @@ GProd (Anonymous, Explicit, rt1, rt2)
let mkRConstruct c = DAst.make @@ GRef (ConstructRef c,None)
@@ -872,7 +872,7 @@ open Util
(** Constructors for constr_expr *)
let mkCProp loc = CAst.make ?loc @@ CSort GProp
-let mkCType loc = CAst.make ?loc @@ CSort (GType [])
+let mkCType loc = CAst.make ?loc @@ CSort (GType UUnknown)
let mkCVar ?loc id = CAst.make ?loc @@ CRef (qualid_of_ident ?loc id, None)
let rec mkCHoles ?loc n =
if n <= 0 then [] else (CAst.make ?loc @@ CHole (None, Namegen.IntroAnonymous, None)) :: mkCHoles ?loc (n - 1)
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 82726eccf0..901a1bd342 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -689,7 +689,7 @@ let hack_qualid_of_univ_level sigma l =
let detype_universe sigma u =
let fn (l, n) =
let qid = hack_qualid_of_univ_level sigma l in
- Some (qid, n)
+ (qid, n)
in
Univ.Universe.map fn u
@@ -700,8 +700,8 @@ let detype_sort sigma = function
| Type u ->
GType
(if !print_universes
- then detype_universe sigma u
- else [])
+ then UNamed (detype_universe sigma u)
+ else UUnknown)
type binder_kind = BProd | BLambda | BLetIn
diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml
index 85b9faac77..656b987942 100644
--- a/pretyping/glob_ops.ml
+++ b/pretyping/glob_ops.ml
@@ -45,14 +45,19 @@ let map_glob_decl_left_to_right f (na,k,obd,ty) =
let comp2 = f ty in
(na,k,comp1,comp2)
-
-let glob_sort_eq g1 g2 = let open Glob_term in match g1, g2 with
-| GSProp, GSProp
-| GProp, GProp
-| GSet, GSet -> true
-| GType l1, GType l2 ->
- List.equal (Option.equal (fun (x,m) (y,n) -> Libnames.qualid_eq x y && Int.equal m n)) l1 l2
-| (GSProp|GProp|GSet|GType _), _ -> false
+let univ_name_eq u1 u2 = match u1, u2 with
+ | UUnknown, UUnknown -> true
+ | UAnonymous, UAnonymous -> true
+ | UNamed l1, UNamed l2 ->
+ List.equal (fun (x,m) (y,n) -> Libnames.qualid_eq x y && Int.equal m n) l1 l2
+ | (UNamed _ | UAnonymous | UUnknown), _ -> false
+
+let glob_sort_eq g1 g2 = match g1, g2 with
+ | GSProp, GSProp
+ | GProp, GProp
+ | GSet, GSet -> true
+ | GType u1, GType u2 -> univ_name_eq u1 u2
+ | (GSProp|GProp|GSet|GType _), _ -> false
let glob_sort_family = let open Sorts in function
| GSProp -> InSProp
diff --git a/pretyping/glob_term.ml b/pretyping/glob_term.ml
index 02cb294f6d..37bacbdeb2 100644
--- a/pretyping/glob_term.ml
+++ b/pretyping/glob_term.ml
@@ -30,15 +30,15 @@ type 'a glob_sort_gen =
| GType of 'a (** representation of [Type] literal *)
type 'a universe_kind =
- | UAnonymous
- | UUnknown
- | UNamed of 'a
+ | UAnonymous (** a flexible universe (collapsable by minimization) *)
+ | UUnknown (** a rigid universe *)
+ | UNamed of 'a (** a named universe or a universe expression *)
-type level_info = Libnames.qualid universe_kind
+type level_info = Libnames.qualid universe_kind (** levels, occurring in universe instances *)
type glob_level = level_info glob_sort_gen
type glob_constraint = glob_level * Univ.constraint_type * glob_level
-type sort_info = (Libnames.qualid * int) option list
+type sort_info = (Libnames.qualid * int) list universe_kind (** sorts: Prop, Set, Type@{...} *)
type glob_sort = sort_info glob_sort_gen
type glob_recarg = int option
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index c7b657f96c..48aba8edf4 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -165,26 +165,27 @@ let interp_universe_level_name ~anon_rigidity evd qid =
in evd, level
let interp_universe ?loc evd = function
- | [] -> let evd, l = new_univ_level_variable ?loc univ_rigid evd in
- evd, Univ.Universe.make l
- | l ->
- List.fold_left (fun (evd, u) l ->
+ | UUnknown ->
+ let evd, l = new_univ_level_variable ?loc univ_rigid evd in
+ evd, Univ.Universe.make l
+ | UAnonymous ->
+ let evd, l = new_univ_level_variable ?loc univ_flexible evd in
+ evd, Univ.Universe.make l
+ | UNamed l ->
+ List.fold_left (fun (evd, u) (l,n) ->
let evd', u' =
- match l with
- | Some (l,n) ->
+ let evd',u' =
(* [univ_flexible_alg] can produce algebraic universes in terms *)
let anon_rigidity = univ_flexible in
let evd', l = interp_universe_level_name ~anon_rigidity evd l in
- let u' = Univ.Universe.make l in
- (match n with
+ evd', Univ.Universe.make l
+ in
+ match n with
| 0 -> evd', u'
| 1 -> evd', Univ.Universe.super u'
- | _ ->
+ | n ->
user_err ?loc ~hdr:"interp_universe"
- (Pp.(str "Cannot interpret universe increment +" ++ int n)))
- | None ->
- let evd, l = new_univ_level_variable ?loc univ_flexible evd in
- evd, Univ.Universe.make l
+ (Pp.(str "Cannot interpret universe increment +" ++ int n))
in (evd', Univ.sup u u'))
(evd, Univ.Universe.type0m) l
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index 8d5213b988..5e64cfb04c 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -157,10 +157,8 @@ let tag_var = tag Tag.variable
let pr_sep_com sep f c = pr_with_comments ?loc:(constr_loc c) (sep() ++ f c)
- let pr_univ_expr = function
- | Some (x,n) ->
- pr_qualid x ++ (match n with 0 -> mt () | _ -> str"+" ++ int n)
- | None -> str"_"
+ let pr_univ_expr (qid,n) =
+ pr_qualid qid ++ (match n with 0 -> mt () | _ -> str"+" ++ int n)
let pr_univ l =
match l with
@@ -173,8 +171,9 @@ let tag_var = tag Tag.variable
| GSProp -> tag_type (str "SProp")
| GProp -> tag_type (str "Prop")
| GSet -> tag_type (str "Set")
- | GType [] -> tag_type (str "Type")
- | GType u -> hov 0 (tag_type (str "Type") ++ pr_univ_annot pr_univ u)
+ | GType UUnknown -> tag_type (str "Type")
+ | GType UAnonymous -> tag_type (str "Type") ++ pr_univ_annot (fun _ -> str "_") ()
+ | GType (UNamed u) -> hov 0 (tag_type (str "Type") ++ pr_univ_annot pr_univ u)
let pr_glob_level = let open Glob_term in function
| GSProp -> tag_type (str "SProp")
diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml
index 977e804da2..2295562a78 100644
--- a/vernac/comInductive.ml
+++ b/vernac/comInductive.ml
@@ -121,7 +121,7 @@ let mk_mltype_data sigma env assums arity indname =
let rec check_anonymous_type ind =
let open Glob_term in
match DAst.get ind with
- | GSort (GType []) -> true
+ | GSort (GType UUnknown) -> true
| GProd ( _, _, _, e)
| GLetIn (_, _, _, e)
| GLambda (_, _, _, e)
@@ -495,7 +495,7 @@ let extract_params indl =
let extract_inductive indl =
List.map (fun ({CAst.v=indname},_,ar,lc) -> {
ind_name = indname;
- ind_arity = Option.cata (fun x -> x) (CAst.make @@ CSort (Glob_term.GType [])) ar;
+ ind_arity = Option.cata (fun x -> x) (CAst.make @@ CSort (Glob_term.GType Glob_term.UUnknown)) ar;
ind_lc = List.map (fun (_,({CAst.v=id},t)) -> (id,t)) lc
}) indl
diff --git a/vernac/record.ml b/vernac/record.ml
index f737a8c524..ead9ed5c90 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -125,7 +125,7 @@ let typecheck_params_and_fields finite def poly pl ps records =
let env = EConstr.push_rel_context newps env0 in
let poly =
match t with
- | { CAst.v = CSort (Glob_term.GType []) } -> true | _ -> false in
+ | { CAst.v = CSort (Glob_term.GType Glob_term.UUnknown) } -> true | _ -> false in
let sigma, s = interp_type_evars ~program_mode:false env sigma ~impls:empty_internalization_env t in
let sred = Reductionops.whd_allnolet env sigma s in
(match EConstr.kind sigma sred with
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 13:02:52 +0000