diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-05-18 15:51:20 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-05-18 15:51:20 +0200 |
| commit | a0da3a68d12141ba226ce94027b90a01389099d0 (patch) | |
| tree | 418ccf3d1b723555bd45ecb647823a5af851097e /vernac | |
| parent | 5281317cb558f2b9aa6f854b9c7aeb617beba8e6 (diff) | |
| parent | a47bd32c261aa1ba6e30ef1b4d08cfc2746ce20f (diff) | |
Merge PR #6965: [api] Move universe syntax to `Glob_term`
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/comInductive.ml | 3 | ||||
| -rw-r--r-- | vernac/record.ml | 2 |
2 files changed, 2 insertions, 3 deletions
diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml index 101298ef4..b2532485a 100644 --- a/vernac/comInductive.ml +++ b/vernac/comInductive.ml @@ -29,7 +29,6 @@ open Indtypes open Pretyping open Evarutil open Indschemes -open Misctypes open Context.Rel.Declaration open Entries @@ -380,7 +379,7 @@ let extract_params indl = let extract_inductive indl = List.map (fun (({CAst.v=indname},pl),_,ar,lc) -> { ind_name = indname; ind_univs = pl; - ind_arity = Option.cata (fun x -> x) (CAst.make @@ CSort (GType [])) ar; + ind_arity = Option.cata (fun x -> x) (CAst.make @@ CSort (Glob_term.GType [])) 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 b89c0060d..b0f229294 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -122,7 +122,7 @@ let typecheck_params_and_fields finite def id poly pl t ps nots fs = let env = EConstr.push_rel_context newps env0 in let poly = match t with - | { CAst.v = CSort (Misctypes.GType []) } -> true | _ -> false in + | { CAst.v = CSort (Glob_term.GType []) } -> true | _ -> false in let sigma, s = interp_type_evars env sigma ~impls:empty_internalization_env t in let sred = Reductionops.whd_allnolet env sigma s in (match EConstr.kind sigma sred with |