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/pattern.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'pretyping/pattern.ml')

diff --git a/pretyping/pattern.ml b/pretyping/pattern.ml
index 7dd0954bc4..996a2dc36a 100644
--- a/pretyping/pattern.ml
+++ b/pretyping/pattern.ml
@@ -30,7 +30,7 @@ type constr_pattern =
   | PLambda of Name.t * constr_pattern * constr_pattern
   | PProd of Name.t * constr_pattern * constr_pattern
   | PLetIn of Name.t * constr_pattern * constr_pattern option * constr_pattern
-  | PSort of glob_sort
+  | PSort of Glob_term.glob_sort
   | PMeta of patvar option
   | PIf of constr_pattern * constr_pattern * constr_pattern
   | PCase of case_info_pattern * constr_pattern * constr_pattern *
-- 
cgit v1.2.3