diff options
Diffstat (limited to 'printing/ppconstr.ml')
| -rw-r--r-- | printing/ppconstr.ml | 40 |
1 files changed, 20 insertions, 20 deletions
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml index e877b3c63..e38da45b9 100644 --- a/printing/ppconstr.ml +++ b/printing/ppconstr.ml @@ -15,15 +15,15 @@ open Pp open CAst open Names open Nameops -open Constr open Libnames open Pputils open Ppextend -open Notation_gram +open Glob_term open Constrexpr open Constrexpr_ops +open Notation_gram open Decl_kinds -open Misctypes +open Namegen (*i*) module Tag = @@ -159,7 +159,7 @@ let tag_var = tag Tag.variable let pr_univ_expr = function | Some (x,n) -> - pr_reference x ++ (match n with 0 -> mt () | _ -> str"+" ++ int n) + pr_qualid x ++ (match n with 0 -> mt () | _ -> str"+" ++ int n) | None -> str"_" let pr_univ l = @@ -180,7 +180,7 @@ let tag_var = tag Tag.variable | GSet -> tag_type (str "Set") | GType UUnknown -> tag_type (str "Type") | GType UAnonymous -> tag_type (str "_") - | GType (UNamed u) -> tag_type (pr_reference u) + | GType (UNamed u) -> tag_type (pr_qualid u) let pr_qualid sp = let (sl, id) = repr_qualid sp in @@ -205,16 +205,16 @@ let tag_var = tag Tag.variable tag_type (str "Set") | GType u -> (match u with - | UNamed u -> pr_reference u + | 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 - let pr_reference = CAst.with_val (function - | Qualid qid -> pr_qualid qid - | Ident id -> tag_var (pr_id id)) + let pr_reference qid = + if qualid_is_ident qid then tag_var (pr_id @@ qualid_basename qid) + else pr_qualid qid let pr_cref ref us = pr_reference ref ++ pr_universe_instance us @@ -228,7 +228,7 @@ let tag_var = tag Tag.variable str "(" ++ pr_id id ++ str ":=" ++ pr ltop a ++ str ")" let pr_opt_type_spc pr = function - | { CAst.v = CHole (_,Misctypes.IntroAnonymous,_) } -> mt () + | { CAst.v = CHole (_,IntroAnonymous,_) } -> mt () | t -> str " :" ++ pr_sep_com (fun()->brk(1,2)) (pr ltop) t let pr_lident {loc; v=id} = @@ -242,8 +242,8 @@ let tag_var = tag Tag.variable | x -> pr_ast Name.print x let pr_or_var pr = function - | ArgArg x -> pr x - | ArgVar id -> pr_lident id + | Locus.ArgArg x -> pr x + | Locus.ArgVar id -> pr_lident id let pr_prim_token = function | Numeral (n,s) -> str (if s then n else "-"^n) @@ -363,7 +363,7 @@ let tag_var = tag Tag.variable end | Default b -> match t with - | { CAst.v = CHole (_,Misctypes.IntroAnonymous,_) } -> + | { CAst.v = CHole (_,IntroAnonymous,_) } -> let s = prlist_with_sep spc pr_lname nal in hov 1 (surround_implicit b s) | _ -> @@ -457,7 +457,7 @@ let tag_var = tag Tag.variable let pr_case_type pr po = match po with - | None | Some { CAst.v = CHole (_,Misctypes.IntroAnonymous,_) } -> mt() + | None | Some { CAst.v = CHole (_,IntroAnonymous,_) } -> mt() | Some p -> spc() ++ hov 2 (keyword "return" ++ pr_sep_com spc (pr lsimpleconstr) p) @@ -564,9 +564,9 @@ let tag_var = tag Tag.variable return (p ++ prlist (pr spc (lapp,L)) l2, lapp) else return (p, lproj) - | CAppExpl ((None,{v=Ident var},us),[t]) - | CApp ((_, {v = CRef({v=Ident var},us)}),[t,None]) - when Id.equal var Notation_ops.ldots_var -> + | CAppExpl ((None,qid,us),[t]) + | CApp ((_, {v = CRef(qid,us)}),[t,None]) + when qualid_is_ident qid && Id.equal (qualid_basename qid) Notation_ops.ldots_var -> return ( hov 0 (str ".." ++ pr spc (latom,E) t ++ spc () ++ str ".."), larg @@ -592,7 +592,7 @@ let tag_var = tag Tag.variable hv 0 (str"{|" ++ pr_record_body_gen (pr spc) l ++ str" |}"), latom ) - | CCases (LetPatternStyle,rtntypopt,[c,as_clause,in_clause],[{v=([[p]],b)}]) -> + | CCases (Constr.LetPatternStyle,rtntypopt,[c,as_clause,in_clause],[{v=([[p]],b)}]) -> return ( hv 0 ( keyword "let" ++ spc () ++ str"'" ++ @@ -643,9 +643,9 @@ let tag_var = tag Tag.variable lif ) - | CHole (_,Misctypes.IntroIdentifier id,_) -> + | CHole (_,IntroIdentifier id,_) -> return (str "?[" ++ pr_id id ++ str "]", latom) - | CHole (_,Misctypes.IntroFresh id,_) -> + | CHole (_,IntroFresh id,_) -> return (str "?[?" ++ pr_id id ++ str "]", latom) | CHole (_,_,_) -> return (str "_", latom) |