From 20c98eab851210702b39e1c66e005acfc351d8dd Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Fri, 1 Dec 2017 10:11:41 +0100 Subject: Proper nametab handling of global universe names They are now bound at the library + module level and can be qualified and shadowed according to the usual rules of qualified names. Parsing and printing of universes "u+n" done as well. In sections, global universes are discharged as well, checking that they can be defined globally when they are introduced --- printing/ppconstr.ml | 19 +++++++++++++------ 1 file changed, 13 insertions(+), 6 deletions(-) (limited to 'printing') diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml index bce5710d6..2abbc389f 100644 --- a/printing/ppconstr.ml +++ b/printing/ppconstr.ml @@ -150,10 +150,15 @@ let tag_var = tag Tag.variable let pr_sep_com sep f c = pr_with_comments ?loc:(constr_loc c) (sep() ++ f c) + let pr_univ_expr = function + | Some (x,n) -> + pr_reference x ++ (match n with 0 -> mt () | _ -> str"+" ++ int n) + | None -> str"_" + let pr_univ l = match l with - | [_,x] -> Name.print x - | l -> str"max(" ++ prlist_with_sep (fun () -> str",") (fun x -> Name.print (snd x)) l ++ str")" + | [x] -> pr_univ_expr x + | l -> str"max(" ++ prlist_with_sep (fun () -> str",") pr_univ_expr l ++ str")" let pr_univ_annot pr x = str "@{" ++ pr x ++ str "}" @@ -166,8 +171,9 @@ let tag_var = tag Tag.variable let pr_glob_level = function | GProp -> tag_type (str "Prop") | GSet -> tag_type (str "Set") - | GType None -> tag_type (str "Type") - | GType (Some (_, u)) -> tag_type (Name.print u) + | GType UUnknown -> tag_type (str "Type") + | GType UAnonymous -> tag_type (str "_") + | GType (UNamed u) -> tag_type (pr_reference u) let pr_qualid sp = let (sl, id) = repr_qualid sp in @@ -192,8 +198,9 @@ let tag_var = tag Tag.variable tag_type (str "Set") | GType u -> (match u with - | Some (_,u) -> Name.print u - | None -> tag_type (str "Type")) + | UNamed u -> pr_reference u + | UAnonymous -> tag_type (str "Type") + | UUnknown -> tag_type (str "_")) let pr_universe_instance l = pr_opt_no_spc (pr_univ_annot (prlist_with_sep spc pr_glob_sort_instance)) l -- cgit v1.2.3