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. --- printing/ppconstr.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'printing/ppconstr.ml') diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml index 412a1cbb4..60268c9de 100644 --- a/printing/ppconstr.ml +++ b/printing/ppconstr.ml @@ -170,13 +170,13 @@ let tag_var = tag Tag.variable let pr_univ_annot pr x = str "@{" ++ pr x ++ str "}" - let pr_glob_sort = function + let pr_glob_sort = let open Glob_term in function | GProp -> tag_type (str "Prop") | GSet -> tag_type (str "Set") | GType [] -> tag_type (str "Type") | GType u -> hov 0 (tag_type (str "Type") ++ pr_univ_annot pr_univ u) - let pr_glob_level = function + let pr_glob_level = let open Glob_term in function | GProp -> tag_type (str "Prop") | GSet -> tag_type (str "Set") | GType UUnknown -> tag_type (str "Type") @@ -199,7 +199,7 @@ let tag_var = tag Tag.variable let pr_qualid = pr_qualid let pr_patvar = pr_id - let pr_glob_sort_instance = function + let pr_glob_sort_instance = let open Glob_term in function | GProp -> tag_type (str "Prop") | GSet -> -- cgit v1.2.3