aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--interp/constrextern.ml13
-rw-r--r--interp/constrintern.ml14
-rw-r--r--interp/declare.mli3
-rw-r--r--interp/notation_ops.ml6
-rw-r--r--parsing/g_constr.mlg42
-rw-r--r--parsing/pcoq.ml1
-rw-r--r--parsing/pcoq.mli1
-rw-r--r--plugins/funind/glob_term_to_relation.ml4
-rw-r--r--plugins/ssr/ssrcommon.ml8
-rw-r--r--pretyping/detyping.ml19
-rw-r--r--pretyping/glob_ops.ml28
-rw-r--r--pretyping/glob_ops.mli7
-rw-r--r--pretyping/glob_term.ml26
-rw-r--r--pretyping/patternops.ml4
-rw-r--r--pretyping/pretyping.ml93
-rw-r--r--pretyping/pretyping.mli2
-rw-r--r--printing/ppconstr.ml49
-rw-r--r--printing/ppconstr.mli1
-rw-r--r--test-suite/bugs/closed/bug_4869.v2
-rw-r--r--vernac/comInductive.ml4
-rw-r--r--vernac/g_vernac.mlg4
-rw-r--r--vernac/ppvernac.ml4
-rw-r--r--vernac/record.ml2
-rw-r--r--vernac/vernacentries.ml2
24 files changed, 172 insertions, 167 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index c05af8be45..701c07dc8d 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -758,8 +758,9 @@ let extended_glob_local_binder_of_decl ?loc u = DAst.make ?loc (extended_glob_lo
let extern_glob_sort = function
(* In case we print a glob_constr w/o having passed through detyping *)
- | GType _ when not !print_universes -> GType UUnknown
- | u -> u
+ | UNamed [(GSProp,0) | (GProp,0) | (GSet,0)] as u -> u
+ | UNamed _ when not !print_universes -> UAnonymous {rigid=true}
+ | UNamed _ | UAnonymous _ as u -> u
let extern_universes = function
| Some _ as l when !print_universes -> l
@@ -1310,10 +1311,10 @@ let rec glob_of_pat avoid env sigma pat = DAst.make @@ match pat with
Array.map (fun (bl,_,_) -> bl) v,
Array.map (fun (_,_,ty) -> ty) v,
Array.map (fun (_,bd,_) -> bd) v)
- | PSort Sorts.InSProp -> GSort GSProp
- | PSort Sorts.InProp -> GSort GProp
- | PSort Sorts.InSet -> GSort GSet
- | PSort Sorts.InType -> GSort (GType UUnknown)
+ | PSort Sorts.InSProp -> GSort (UNamed [GSProp,0])
+ | PSort Sorts.InProp -> GSort (UNamed [GProp,0])
+ | PSort Sorts.InSet -> GSort (UNamed [GSet,0])
+ | PSort Sorts.InType -> GSort (UAnonymous {rigid=true})
| PInt i -> GInt i
let extern_constr_pattern env sigma pat =
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index b4294b4ff8..1a81dc41a1 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -998,18 +998,10 @@ let intern_reference qid =
in
Smartlocate.global_of_extended_global r
-let sort_info_of_level_info (info: level_info) : sort_info =
- match info with
- | 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)
+ | UAnonymous {rigid} -> UAnonymous {rigid}
+ | UNamed id -> UNamed [id,0]
(* Is it a global reference or a syntactic definition? *)
let intern_qualid ?(no_secvar=false) qid intern env ntnvars us args =
@@ -1045,7 +1037,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 UUnknown) -> DAst.make ?loc @@ GSort (glob_sort_of_level s)
+ | Some [s], GSort (UAnonymous {rigid=true}) -> 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/interp/declare.mli b/interp/declare.mli
index 795d9a767d..0b1a396a34 100644
--- a/interp/declare.mli
+++ b/interp/declare.mli
@@ -90,5 +90,4 @@ val declare_univ_binders : GlobRef.t -> UnivNames.universe_binders -> unit
val declare_universe_context : polymorphic -> Univ.ContextSet.t -> unit
val do_universe : polymorphic -> lident list -> unit
-val do_constraint : polymorphic -> (Glob_term.glob_level * Univ.constraint_type * Glob_term.glob_level) list ->
- unit
+val do_constraint : polymorphic -> Glob_term.glob_constraint list -> unit
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index 7f084fffdd..08619d912e 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -1190,7 +1190,11 @@ let rec match_ inner u alp metas sigma a1 a2 =
Array.fold_left2 (match_in u alp metas) sigma bl1 bl2
| GCast(t1, c1), NCast(t2, c2) ->
match_cast (match_in u alp metas) (match_in u alp metas sigma t1 t2) c1 c2
- | GSort (GType _), NSort (GType _) when not u -> sigma
+
+ (* Next pair of lines useful only if not coming from detyping *)
+ | GSort (UNamed [(GProp|GSet),0]), NSort (UAnonymous _) -> raise No_match
+ | GSort _, NSort (UAnonymous _) when not u -> sigma
+
| GSort s1, NSort s2 when glob_sort_eq s1 s2 -> sigma
| GInt i1, NInt i2 when Uint63.equal i1 i2 -> sigma
| GPatVar _, NHole _ -> (*Don't hide Metas, they bind in ltac*) raise No_match
diff --git a/parsing/g_constr.mlg b/parsing/g_constr.mlg
index dd68b411a0..79cfe33b12 100644
--- a/parsing/g_constr.mlg
+++ b/parsing/g_constr.mlg
@@ -133,7 +133,8 @@ let aliasvar = function { CAst.v = CPatAlias (_, na) } -> Some na | _ -> None
}
GRAMMAR EXTEND Gram
- GLOBAL: binder_constr lconstr constr operconstr universe_level sort sort_family
+ GLOBAL: binder_constr lconstr constr operconstr
+ universe_level universe_name sort sort_family
global constr_pattern lconstr_pattern Constr.ident
closed_binder open_binders binder binders binders_fixannot
record_declaration typeclass_constraint pattern appl_arg;
@@ -153,11 +154,12 @@ GRAMMAR EXTEND Gram
[ [ c = lconstr -> { c } ] ]
;
sort:
- [ [ "Set" -> { GSet }
- | "Prop" -> { GProp }
- | "SProp" -> { GSProp }
- | "Type" -> { GType UUnknown }
- | "Type"; "@{"; u = universe; "}" -> { GType u }
+ [ [ "Set" -> { UNamed [GSet,0] }
+ | "Prop" -> { UNamed [GProp,0] }
+ | "SProp" -> { UNamed [GSProp,0] }
+ | "Type" -> { UAnonymous {rigid=true} }
+ | "Type"; "@{"; "_"; "}" -> { UAnonymous {rigid=false} }
+ | "Type"; "@{"; u = universe; "}" -> { UNamed u }
] ]
;
sort_family:
@@ -167,15 +169,21 @@ GRAMMAR EXTEND Gram
| "Type" -> { Sorts.InType }
] ]
;
+ universe_increment:
+ [ [ "+"; n = natural -> { n }
+ | -> { 0 } ] ]
+ ;
+ universe_name:
+ [ [ id = global -> { GType id }
+ | "Set" -> { GSet }
+ | "Prop" -> { GProp } ] ]
+ ;
universe_expr:
- [ [ id = global; "+"; n = natural -> { (id,n) }
- | id = global -> { (id,0) }
- ] ]
+ [ [ id = universe_name; n = universe_increment -> { (id,n) } ] ]
;
universe:
- [ [ IDENT "max"; "("; ids = LIST1 universe_expr SEP ","; ")" -> { UNamed ids }
- | u = universe_expr -> { UNamed [u] }
- | "_" -> { UAnonymous }
+ [ [ IDENT "max"; "("; ids = LIST1 universe_expr SEP ","; ")" -> { ids }
+ | u = universe_expr -> { [u] }
] ]
;
lconstr:
@@ -328,12 +336,12 @@ GRAMMAR EXTEND Gram
| -> { None } ] ]
;
universe_level:
- [ [ "Set" -> { GSet }
+ [ [ "Set" -> { UNamed GSet }
(* no parsing SProp as a level *)
- | "Prop" -> { GProp }
- | "Type" -> { GType UUnknown }
- | "_" -> { GType UAnonymous }
- | id = global -> { GType (UNamed id) }
+ | "Prop" -> { UNamed GProp }
+ | "Type" -> { UAnonymous {rigid=true} }
+ | "_" -> { UAnonymous {rigid=false} }
+ | id = global -> { UNamed (GType id) }
] ]
;
fix_constr:
diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index b474c8e9a9..b375c526ad 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -427,6 +427,7 @@ module Constr =
let binder_constr = gec_constr "binder_constr"
let ident = make_gen_entry uconstr "ident"
let global = make_gen_entry uconstr "global"
+ let universe_name = make_gen_entry uconstr "universe_name"
let universe_level = make_gen_entry uconstr "universe_level"
let sort = make_gen_entry uconstr "sort"
let sort_family = make_gen_entry uconstr "sort_family"
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index 5f982346ab..196835f184 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -182,6 +182,7 @@ module Constr :
val operconstr : constr_expr Entry.t
val ident : Id.t Entry.t
val global : qualid Entry.t
+ val universe_name : Glob_term.glob_sort_name Entry.t
val universe_level : Glob_term.glob_level Entry.t
val sort : Glob_term.glob_sort Entry.t
val sort_family : Sorts.family Entry.t
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index 889a2d7359..201d953692 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -1299,10 +1299,10 @@ let rec rebuild_return_type rt =
| Constrexpr.CProdN(n,t') ->
CAst.make ?loc @@ Constrexpr.CProdN(n,rebuild_return_type t')
| Constrexpr.CLetIn(na,v,t,t') ->
- CAst.make ?loc @@ Constrexpr.CLetIn(na,v,t,rebuild_return_type t')
+ 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 UUnknown))
+ CAst.make @@ Constrexpr.CSort(UAnonymous {rigid=true}))
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 4470c36888..935620239b 100644
--- a/plugins/ssr/ssrcommon.ml
+++ b/plugins/ssr/ssrcommon.ml
@@ -194,8 +194,8 @@ 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 UUnknown)
-let mkRProp = DAst.make @@ GSort (GProp)
+let mkRType = DAst.make @@ GSort (UAnonymous {rigid=true})
+let mkRProp = DAst.make @@ GSort (UNamed [GProp,0])
let mkRArrow rt1 rt2 = DAst.make @@ GProd (Anonymous, Explicit, rt1, rt2)
let mkRConstruct c = DAst.make @@ GRef (ConstructRef c,None)
let mkRInd mind = DAst.make @@ GRef (IndRef mind,None)
@@ -871,8 +871,8 @@ open Constrexpr
open Util
(** Constructors for constr_expr *)
-let mkCProp loc = CAst.make ?loc @@ CSort GProp
-let mkCType loc = CAst.make ?loc @@ CSort (GType UUnknown)
+let mkCProp loc = CAst.make ?loc @@ CSort (UNamed [GProp,0])
+let mkCType loc = CAst.make ?loc @@ CSort (UAnonymous {rigid=true})
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 901a1bd342..18a036cb8c 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -688,20 +688,21 @@ 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
- (qid, n)
- in
+ let s =
+ if Univ.Level.is_prop l then GProp else
+ if Univ.Level.is_set l then GSet else
+ GType (hack_qualid_of_univ_level sigma l) in
+ (s, n) in
Univ.Universe.map fn u
let detype_sort sigma = function
- | SProp -> GSProp
- | Prop -> GProp
- | Set -> GSet
+ | SProp -> UNamed [GSProp,0]
+ | Prop -> UNamed [GProp,0]
+ | Set -> UNamed [GSet,0]
| Type u ->
- GType
(if !print_universes
then UNamed (detype_universe sigma u)
- else UUnknown)
+ else UAnonymous {rigid=true})
type binder_kind = BProd | BLambda | BLetIn
@@ -710,7 +711,7 @@ type binder_kind = BProd | BLambda | BLetIn
let detype_level sigma l =
let l = hack_qualid_of_univ_level sigma l in
- GType (UNamed l)
+ UNamed (GType l)
let detype_instance sigma l =
let l = EInstance.kind sigma l in
diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml
index 656b987942..a3a3c7f811 100644
--- a/pretyping/glob_ops.ml
+++ b/pretyping/glob_ops.ml
@@ -45,25 +45,27 @@ let map_glob_decl_left_to_right f (na,k,obd,ty) =
let comp2 = f ty in
(na,k,comp1,comp2)
-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
+let glob_sort_name_eq g1 g2 = match g1, g2 with
| GSProp, GSProp
| GProp, GProp
| GSet, GSet -> true
- | GType u1, GType u2 -> univ_name_eq u1 u2
+ | GType u1, GType u2 -> Libnames.qualid_eq u1 u2
| (GSProp|GProp|GSet|GType _), _ -> false
+exception ComplexSort
+
let glob_sort_family = let open Sorts in function
-| GSProp -> InSProp
-| GProp -> InProp
-| GSet -> InSet
-| GType _ -> InType
+ | UAnonymous {rigid=true} -> InType
+ | UNamed [GSProp,0] -> InProp
+ | UNamed [GProp,0] -> InProp
+ | UNamed [GSet,0] -> InSet
+ | _ -> raise ComplexSort
+
+let glob_sort_eq u1 u2 = match u1, u2 with
+ | UAnonymous {rigid=r1}, UAnonymous {rigid=r2} -> r1 = r2
+ | UNamed l1, UNamed l2 ->
+ List.equal (fun (x,m) (y,n) -> glob_sort_name_eq x y && Int.equal m n) l1 l2
+ | (UNamed _ | UAnonymous _), _ -> false
let binding_kind_eq bk1 bk2 = match bk1, bk2 with
| Decl_kinds.Explicit, Decl_kinds.Explicit -> true
diff --git a/pretyping/glob_ops.mli b/pretyping/glob_ops.mli
index df902a8fa7..3995ab6a5a 100644
--- a/pretyping/glob_ops.mli
+++ b/pretyping/glob_ops.mli
@@ -15,10 +15,13 @@ open Glob_term
val glob_sort_eq : Glob_term.glob_sort -> Glob_term.glob_sort -> bool
-val glob_sort_family : 'a glob_sort_gen -> Sorts.family
-
val cases_pattern_eq : 'a cases_pattern_g -> 'a cases_pattern_g -> bool
+(** Expect a Prop/SProp/Set/Type universe; raise [ComplexSort] if
+ contains a max, an increment, or a flexible universe *)
+exception ComplexSort
+val glob_sort_family : glob_sort -> Sorts.family
+
val alias_of_pat : 'a cases_pattern_g -> Name.t
val set_pat_alias : Id.t -> 'a cases_pattern_g -> 'a cases_pattern_g
diff --git a/pretyping/glob_term.ml b/pretyping/glob_term.ml
index 37bacbdeb2..704cddd784 100644
--- a/pretyping/glob_term.ml
+++ b/pretyping/glob_term.ml
@@ -23,23 +23,23 @@ type existential_name = Id.t
(** Sorts *)
-type 'a glob_sort_gen =
+type glob_sort_name =
| GSProp (** representation of [SProp] literal *)
- | GProp (** representation of [Prop] literal *)
- | GSet (** representation of [Set] literal *)
- | GType of 'a (** representation of [Type] literal *)
+ | GProp (** representation of [Prop] level *)
+ | GSet (** representation of [Set] level *)
+ | GType of Libnames.qualid (** representation of a [Type] level *)
-type 'a universe_kind =
- | UAnonymous (** a flexible universe (collapsable by minimization) *)
- | UUnknown (** a rigid universe *)
- | UNamed of 'a (** a named universe or a universe expression *)
+type 'a glob_sort_expr =
+ | UAnonymous of { rigid : bool } (** not rigid = unifiable by minimization *)
+ | UNamed of 'a
-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
+(** levels, occurring in universe instances *)
+type glob_level = glob_sort_name glob_sort_expr
-type sort_info = (Libnames.qualid * int) list universe_kind (** sorts: Prop, Set, Type@{...} *)
-type glob_sort = sort_info glob_sort_gen
+(** sort expressions *)
+type glob_sort = (glob_sort_name * int) list glob_sort_expr
+
+type glob_constraint = glob_sort_name * Univ.constraint_type * glob_sort_name
type glob_recarg = int option
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index c788efda48..2d27b27cab 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -410,7 +410,9 @@ let rec pat_of_raw metas vars = DAst.with_loc_val (fun ?loc -> function
PLetIn (na, pat_of_raw metas vars c1,
Option.map (pat_of_raw metas vars) t,
pat_of_raw metas (na::vars) c2)
- | GSort gs -> PSort (Glob_ops.glob_sort_family gs)
+ | GSort gs ->
+ (try PSort (Glob_ops.glob_sort_family gs)
+ with Glob_ops.ComplexSort -> user_err ?loc (str "Unexpected universe in pattern."))
| GHole _ ->
PMeta None
| GCast (c,_) ->
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 48aba8edf4..be8f7215fa 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -132,7 +132,7 @@ let is_strict_universe_declarations =
(** Miscellaneous interpretation functions *)
-let interp_known_universe_level evd qid =
+let interp_known_universe_level_name evd qid =
try
let open Libnames in
if qualid_is_ident qid then Evd.universe_of_name evd @@ qualid_basename qid
@@ -142,7 +142,7 @@ let interp_known_universe_level evd qid =
Univ.Level.make qid
let interp_universe_level_name ~anon_rigidity evd qid =
- try evd, interp_known_universe_level evd qid
+ try evd, interp_known_universe_level_name evd qid
with Not_found ->
if Libnames.qualid_is_ident qid then (* Undeclared *)
let id = Libnames.qualid_basename qid in
@@ -164,45 +164,31 @@ let interp_universe_level_name ~anon_rigidity evd qid =
with UGraph.AlreadyDeclared -> evd
in evd, level
-let interp_universe ?loc evd = function
- | 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 ->
+let interp_universe_name ?loc evd l =
+ (* [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
+ evd', l
+
+let interp_sort_name ?loc sigma = function
+ | GSProp -> sigma, Univ.Level.sprop
+ | GProp -> sigma, Univ.Level.prop
+ | GSet -> sigma, Univ.Level.set
+ | GType l -> interp_universe_name ?loc sigma l
+
+let interp_sort_info ?loc evd l =
List.fold_left (fun (evd, u) (l,n) ->
- let evd', u' =
- 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
- 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))
+ let evd', u' = interp_sort_name ?loc evd l in
+ let u' = Univ.Universe.make u' in
+ let u' = match n with
+ | 0 -> u'
+ | 1 -> Univ.Universe.super u'
+ | n ->
+ user_err ?loc ~hdr:"interp_universe"
+ (Pp.(str "Cannot interpret universe increment +" ++ int n))
in (evd', Univ.sup u u'))
(evd, Univ.Universe.type0m) l
-let interp_known_level_info ?loc evd = function
- | UUnknown | UAnonymous ->
- user_err ?loc ~hdr:"interp_known_level_info"
- (str "Anonymous universes not allowed here.")
- | UNamed qid ->
- try interp_known_universe_level evd qid
- with Not_found ->
- user_err ?loc ~hdr:"interp_known_level_info" (str "Undeclared universe " ++ Libnames.pr_qualid qid)
-
-let interp_level_info ?loc evd : level_info -> _ = function
- | UUnknown -> new_univ_level_variable ?loc univ_rigid evd
- | UAnonymous -> new_univ_level_variable ?loc univ_flexible evd
- | UNamed s -> interp_universe_level_name ~anon_rigidity:univ_flexible evd s
-
type inference_hook = env -> evar_map -> Evar.t -> evar_map * constr
type inference_flags = {
@@ -416,13 +402,14 @@ let interp_known_glob_level ?loc evd = function
| GSProp -> Univ.Level.sprop
| GProp -> Univ.Level.prop
| GSet -> Univ.Level.set
- | GType s -> interp_known_level_info ?loc evd s
+ | GType qid ->
+ try interp_known_universe_level_name evd qid
+ with Not_found ->
+ user_err ?loc ~hdr:"interp_known_level_info" (str "Undeclared universe " ++ Libnames.pr_qualid qid)
let interp_glob_level ?loc evd : glob_level -> _ = function
- | GSProp -> evd, Univ.Level.sprop
- | GProp -> evd, Univ.Level.prop
- | GSet -> evd, Univ.Level.set
- | GType s -> interp_level_info ?loc evd s
+ | UAnonymous {rigid} -> new_univ_level_variable ?loc (if rigid then univ_rigid else univ_flexible) evd
+ | UNamed s -> interp_sort_name ?loc evd s
let interp_instance ?loc evd l =
let evd, l' =
@@ -461,18 +448,26 @@ let pretype_ref ?loc sigma env ref us =
let ty = unsafe_type_of !!env sigma c in
sigma, make_judge c ty
-let judge_of_Type ?loc evd s =
- let evd, s = interp_universe ?loc evd s in
+let interp_sort ?loc evd : glob_sort -> _ = function
+ | UAnonymous {rigid} ->
+ let evd, l = new_univ_level_variable ?loc (if rigid then univ_rigid else univ_flexible) evd in
+ evd, Univ.Universe.make l
+ | UNamed l -> interp_sort_info ?loc evd l
+
+let judge_of_sort ?loc evd s =
let judge =
{ uj_val = mkType s; uj_type = mkType (Univ.super s) }
in
evd, judge
-let pretype_sort ?loc sigma = function
- | GSProp -> sigma, judge_of_sprop
- | GProp -> sigma, judge_of_prop
- | GSet -> sigma, judge_of_set
- | GType s -> judge_of_Type ?loc sigma s
+let pretype_sort ?loc sigma s =
+ match s with
+ | UNamed [GSProp,0] -> sigma, judge_of_sprop
+ | UNamed [GProp,0] -> sigma, judge_of_prop
+ | UNamed [GSet,0] -> sigma, judge_of_set
+ | _ ->
+ let sigma, s = interp_sort ?loc sigma s in
+ judge_of_sort ?loc sigma s
let new_type_evar env sigma loc =
new_type_evar env sigma ~src:(Loc.tag ?loc Evar_kinds.InternalHole)
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index c0a95e73c6..d38aafd0e9 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -31,7 +31,7 @@ val get_bidirectionality_hint : GlobRef.t -> int option
val clear_bidirectionality_hint : GlobRef.t -> unit
val interp_known_glob_level : ?loc:Loc.t -> Evd.evar_map ->
- glob_level -> Univ.Level.t
+ glob_sort_name -> Univ.Level.t
(** An auxiliary function for searching for fixpoint guard indexes *)
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index 5e64cfb04c..27ed2189ed 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -157,8 +157,14 @@ 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 (qid,n) =
- pr_qualid qid ++ (match n with 0 -> mt () | _ -> str"+" ++ int n)
+ let pr_glob_sort_name = function
+ | GSProp -> str "SProp"
+ | GProp -> str "Prop"
+ | GSet -> str "Set"
+ | GType qid -> pr_qualid qid
+
+ let pr_univ_expr (u,n) =
+ pr_glob_sort_name u ++ (match n with 0 -> mt () | _ -> str"+" ++ int n)
let pr_univ l =
match l with
@@ -168,20 +174,20 @@ let tag_var = tag Tag.variable
let pr_univ_annot pr x = str "@{" ++ pr x ++ str "}"
let pr_glob_sort = let open Glob_term in function
- | GSProp -> tag_type (str "SProp")
- | GProp -> tag_type (str "Prop")
- | GSet -> tag_type (str "Set")
- | 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)
+ | UNamed [GSProp,0] -> tag_type (str "SProp")
+ | UNamed [GProp,0] -> tag_type (str "Prop")
+ | UNamed [GSet,0] -> tag_type (str "Set")
+ | UAnonymous {rigid=true} -> tag_type (str "Type")
+ | UAnonymous {rigid=false} -> tag_type (str "Type") ++ pr_univ_annot (fun _ -> str "_") ()
+ | 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")
- | GProp -> tag_type (str "Prop")
- | GSet -> tag_type (str "Set")
- | GType UUnknown -> tag_type (str "Type")
- | GType UAnonymous -> tag_type (str "_")
- | GType (UNamed u) -> tag_type (pr_qualid u)
+ | UNamed GSProp -> tag_type (str "SProp")
+ | UNamed GProp -> tag_type (str "Prop")
+ | UNamed GSet -> tag_type (str "Set")
+ | UAnonymous {rigid=true} -> tag_type (str "Type")
+ | UAnonymous {rigid=false} -> tag_type (str "_")
+ | UNamed (GType u) -> tag_type (pr_qualid u)
let pr_qualid sp =
let (sl, id) = repr_qualid sp in
@@ -198,21 +204,8 @@ let tag_var = tag Tag.variable
let pr_qualid = pr_qualid
let pr_patvar = pr_id
- let pr_glob_sort_instance = let open Glob_term in function
- | GSProp ->
- tag_type (str "SProp")
- | GProp ->
- tag_type (str "Prop")
- | GSet ->
- tag_type (str "Set")
- | GType u ->
- (match u with
- | UNamed u -> pr_qualid u
- | UAnonymous -> tag_type (str "Type")
- | UUnknown -> tag_type (str "_"))
-
let pr_universe_instance l =
- pr_opt_no_spc (pr_univ_annot (prlist_with_sep spc pr_glob_sort_instance)) l
+ pr_opt_no_spc (pr_univ_annot (prlist_with_sep spc pr_glob_level)) l
let pr_reference qid =
if qualid_is_ident qid then tag_var (pr_id @@ qualid_basename qid)
diff --git a/printing/ppconstr.mli b/printing/ppconstr.mli
index 1332cd0168..219fe4336a 100644
--- a/printing/ppconstr.mli
+++ b/printing/ppconstr.mli
@@ -33,6 +33,7 @@ val pr_id : Id.t -> Pp.t
val pr_qualid : qualid -> Pp.t
val pr_patvar : Pattern.patvar -> Pp.t
+val pr_glob_sort_name : Glob_term.glob_sort_name -> Pp.t
val pr_glob_level : Glob_term.glob_level -> Pp.t
val pr_glob_sort : Glob_term.glob_sort -> Pp.t
val pr_guard_annot
diff --git a/test-suite/bugs/closed/bug_4869.v b/test-suite/bugs/closed/bug_4869.v
index ac5d7ea287..1fe91de72d 100644
--- a/test-suite/bugs/closed/bug_4869.v
+++ b/test-suite/bugs/closed/bug_4869.v
@@ -6,7 +6,9 @@ Fail Constraint i = Set.
Constraint Set <= i.
Constraint Set < i.
Fail Constraint i < j. (* undeclared j *)
+(* Now a parsing error
Fail Constraint i < Type. (* anonymous *)
+*)
Set Universe Polymorphism.
diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml
index 2295562a78..5bebf955ec 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 UUnknown) -> true
+ | GSort (UAnonymous {rigid=true}) -> 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 Glob_term.UUnknown)) ar;
+ ind_arity = Option.cata (fun x -> x) (CAst.make @@ CSort (Glob_term.UAnonymous {rigid=true})) ar;
ind_lc = List.map (fun (_,({CAst.v=id},t)) -> (id,t)) lc
}) indl
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index 5eec8aed1e..a8d7b6f217 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -296,8 +296,8 @@ GRAMMAR EXTEND Gram
| -> { NoInline } ] ]
;
univ_constraint:
- [ [ l = universe_level; ord = [ "<" -> { Univ.Lt } | "=" -> { Univ.Eq } | "<=" -> { Univ.Le } ];
- r = universe_level -> { (l, ord, r) } ] ]
+ [ [ l = universe_name; ord = [ "<" -> { Univ.Lt } | "=" -> { Univ.Eq } | "<=" -> { Univ.Le } ];
+ r = universe_name -> { (l, ord, r) } ] ]
;
univ_decl :
[ [ "@{" ; l = LIST0 identref; ext = [ "+" -> { true } | -> { false } ];
diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml
index e307c0c268..80e6c9d337 100644
--- a/vernac/ppvernac.ml
+++ b/vernac/ppvernac.ml
@@ -39,8 +39,8 @@ open Pputils
pr_sep_com spc @@ pr_lconstr_expr env sigma
let pr_uconstraint (l, d, r) =
- pr_glob_level l ++ spc () ++ Univ.pr_constraint_type d ++ spc () ++
- pr_glob_level r
+ pr_glob_sort_name l ++ spc () ++ Univ.pr_constraint_type d ++ spc () ++
+ pr_glob_sort_name r
let pr_univ_name_list = function
| None -> mt ()
diff --git a/vernac/record.ml b/vernac/record.ml
index ead9ed5c90..c8c482531a 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 Glob_term.UUnknown) } -> true | _ -> false in
+ | { CAst.v = CSort (Glob_term.UAnonymous {rigid=true}) } -> 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
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 22427621e6..2cd40ee63b 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -405,7 +405,7 @@ let universe_subgraph ?loc g univ =
let open Univ in
let sigma = Evd.from_env (Global.env()) in
let univs_of q =
- let q = Glob_term.(GType (UNamed q)) in
+ let q = Glob_term.(GType q) in
(* this function has a nice error message for not found univs *)
LSet.singleton (Pretyping.interp_known_glob_level ?loc sigma q)
in
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 12:24:18 +0000