diff options
| author | Gaëtan Gilbert | 2019-06-06 13:27:40 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-06-06 13:27:40 +0200 |
| commit | 90c1084ba489415f8df588c43e088491bc6be450 (patch) | |
| tree | 0489f116505f9956d7fd076937038009dbc0485e /vernac | |
| parent | 4f7af2b09a935528d660a354f5e7672fc92e9a5c (diff) | |
| parent | 1ac8d4751317d50b01a53980b09f36c5dc30c8e3 (diff) | |
Merge PR #8988: Towards unifying parsing/printing for universe instances and Type's argument
Reviewed-by: SkySkimmer
Reviewed-by: gares
Reviewed-by: mattam82
Reviewed-by: maximedenes
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/comInductive.ml | 4 | ||||
| -rw-r--r-- | vernac/g_vernac.mlg | 4 | ||||
| -rw-r--r-- | vernac/ppvernac.ml | 4 | ||||
| -rw-r--r-- | vernac/record.ml | 2 | ||||
| -rw-r--r-- | vernac/vernacentries.ml | 2 |
5 files changed, 8 insertions, 8 deletions
diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml index 977e804da2..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 []) -> 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 [])) 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 63e6dd247f..cec68b89bc 100644 --- a/vernac/g_vernac.mlg +++ b/vernac/g_vernac.mlg @@ -295,8 +295,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 535a0fa02c..02af1904fd 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 d617b13db4..6101e13edd 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.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 18e0fde296..af13c873e2 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -429,7 +429,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 |