From a47bd32c261aa1ba6e30ef1b4d08cfc2746ce20f Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Tue, 24 Apr 2018 03:26:40 +0200 Subject: [api] Move universe syntax to `Glob_term` We move syntax for universes from `Misctypes` to `Glob_term`. There is basically no reason that this type is there instead of the proper file, as witnessed by the diff. Unfortunately the change is not compatible due to moving a type to a higher level in the hierarchy, but we expect few problems. This change plus the related PR (#6515) moving universe declaration to their proper place make `Misctypes` into basically an empty file save for introduction patterns. --- vernac/comInductive.ml | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) (limited to 'vernac/comInductive.ml') 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 -- cgit v1.2.3