diff options
Diffstat (limited to 'printing/ppconstr.ml')
| -rw-r--r-- | printing/ppconstr.ml | 57 |
1 files changed, 25 insertions, 32 deletions
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml index 9d3ed40f6c..27ed2189ed 100644 --- a/printing/ppconstr.ml +++ b/printing/ppconstr.ml @@ -157,10 +157,14 @@ 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_qualid x ++ (match n with 0 -> mt () | _ -> str"+" ++ int n) - | None -> str"_" + let pr_glob_sort_name = function + | GSProp -> str "SProp" + | GProp -> str "Prop" + | GSet -> str "Set" + | GType qid -> pr_qualid qid + + let pr_univ_expr (u,n) = + pr_glob_sort_name u ++ (match n with 0 -> mt () | _ -> str"+" ++ int n) let pr_univ l = match l with @@ -170,19 +174,20 @@ let tag_var = tag Tag.variable let pr_univ_annot pr x = str "@{" ++ pr x ++ str "}" let pr_glob_sort = let open Glob_term in function - | GSProp -> tag_type (str "SProp") - | 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) + | UNamed [GSProp,0] -> tag_type (str "SProp") + | UNamed [GProp,0] -> tag_type (str "Prop") + | UNamed [GSet,0] -> tag_type (str "Set") + | UAnonymous {rigid=true} -> tag_type (str "Type") + | UAnonymous {rigid=false} -> tag_type (str "Type") ++ pr_univ_annot (fun _ -> str "_") () + | UNamed u -> hov 0 (tag_type (str "Type") ++ pr_univ_annot pr_univ u) let pr_glob_level = let open Glob_term in function - | GSProp -> tag_type (str "SProp") - | GProp -> tag_type (str "Prop") - | GSet -> tag_type (str "Set") - | GType UUnknown -> tag_type (str "Type") - | GType UAnonymous -> tag_type (str "_") - | GType (UNamed u) -> tag_type (pr_qualid u) + | UNamed GSProp -> tag_type (str "SProp") + | UNamed GProp -> tag_type (str "Prop") + | UNamed GSet -> tag_type (str "Set") + | UAnonymous {rigid=true} -> tag_type (str "Type") + | UAnonymous {rigid=false} -> tag_type (str "_") + | UNamed (GType u) -> tag_type (pr_qualid u) let pr_qualid sp = let (sl, id) = repr_qualid sp in @@ -199,21 +204,8 @@ let tag_var = tag Tag.variable let pr_qualid = pr_qualid let pr_patvar = pr_id - let pr_glob_sort_instance = let open Glob_term in function - | GSProp -> - tag_type (str "SProp") - | GProp -> - tag_type (str "Prop") - | GSet -> - tag_type (str "Set") - | GType u -> - (match u with - | UNamed u -> pr_qualid 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 + pr_opt_no_spc (pr_univ_annot (prlist_with_sep spc pr_glob_level)) l let pr_reference qid = if qualid_is_ident qid then tag_var (pr_id @@ qualid_basename qid) @@ -249,7 +241,7 @@ let tag_var = tag Tag.variable str"@{" ++ hov 0 (prlist_with_sep pr_semicolon f (List.rev l)) ++ str"}")) let las = lapp - let lpator = 100 + let lpator = 0 let lpatrec = 0 let rec pr_patt sep inh p = @@ -283,7 +275,8 @@ let tag_var = tag Tag.variable pr_reference r, latom | CPatOr pl -> - hov 0 (prlist_with_sep pr_spcbar (pr_patt mt (lpator,L)) pl), lpator + let pp = pr_patt mt (lpator,Any) in + surround (hov 0 (prlist_with_sep pr_spcbar pp pl)), lpator | CPatNotation ((_,"( _ )"),([p],[]),[]) -> pr_patt (fun()->str"(") (max_int,E) p ++ str")", latom @@ -348,7 +341,7 @@ let tag_var = tag Tag.variable hov 1 (str "`" ++ (surround_impl b' (pr_lident CAst.(make ?loc id) ++ str " : " ++ (if t' then str "!" else mt()) ++ pr t))) - |_ -> anomaly (Pp.str "List of generalized binders have alwais one element.") + |_ -> anomaly (Pp.str "List of generalized binders have always one element.") end | Default b -> match t with |