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.
---
 pretyping/constrexpr.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'pretyping/constrexpr.ml')

diff --git a/pretyping/constrexpr.ml b/pretyping/constrexpr.ml
index fda31756a9..1443dfb513 100644
--- a/pretyping/constrexpr.ml
+++ b/pretyping/constrexpr.ml
@@ -17,7 +17,7 @@ open Decl_kinds
 
 (** [constr_expr] is the abstract syntax tree produced by the parser *)
 
-type universe_decl_expr = (lident list, glob_constraint list) gen_universe_decl
+type universe_decl_expr = (lident list, Glob_term.glob_constraint list) gen_universe_decl
 
 type ident_decl = lident * universe_decl_expr option
 type name_decl = lname * universe_decl_expr option
@@ -50,7 +50,7 @@ type prim_token =
   | Numeral of raw_natural_number * sign
   | String of string
 
-type instance_expr = Misctypes.glob_level list
+type instance_expr = Glob_term.glob_level list
 
 type cases_pattern_expr_r =
   | CPatAlias of cases_pattern_expr * lname
@@ -98,7 +98,7 @@ and constr_expr_r =
   | CHole   of Evar_kinds.t option * intro_pattern_naming_expr * Genarg.raw_generic_argument option
   | CPatVar of patvar
   | CEvar   of Glob_term.existential_name * (Id.t * constr_expr) list
-  | CSort   of glob_sort
+  | CSort   of Glob_term.glob_sort
   | CCast   of constr_expr * constr_expr cast_type
   | CNotation of notation * constr_notation_substitution
   | CGeneralization of binding_kind * abstraction_kind option * constr_expr
-- 
cgit v1.2.3