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/constr_matching.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'pretyping/constr_matching.ml') diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml index 89d490a41..57ca03f5e 100644 --- a/pretyping/constr_matching.ml +++ b/pretyping/constr_matching.ml @@ -20,7 +20,6 @@ open EConstr open Vars open Pattern open Patternops -open Misctypes open Context.Rel.Declaration open Ltac_pretype (*i*) @@ -277,6 +276,7 @@ let matches_core env sigma allow_bound_rels | PSort ps, Sort s -> + let open Glob_term in begin match ps, ESorts.kind sigma s with | GProp, Prop Null -> subst | GSet, Prop Pos -> subst -- cgit v1.2.3