diff options
Diffstat (limited to 'printing/ppvernac.ml')
| -rw-r--r-- | printing/ppvernac.ml | 25 |
1 files changed, 14 insertions, 11 deletions
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 51fc289b4..1cdf55ac6 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -365,8 +365,8 @@ module Make | SetAssoc NonA -> keyword "no associativity" | SetEntryType (x,typ) -> str x ++ spc() ++ pr_set_entry_type typ | SetOnlyPrinting -> keyword "only printing" - | SetOnlyParsing Flags.Current -> keyword "only parsing" - | SetOnlyParsing v -> keyword("compat \"" ^ Flags.pr_version v ^ "\"") + | SetOnlyParsing -> keyword "only parsing" + | SetCompatVersion v -> keyword("compat \"" ^ Flags.pr_version v ^ "\"") | SetFormat("text",s) -> keyword "format " ++ pr_located qs s | SetFormat(k,s) -> keyword "format " ++ qs k ++ spc() ++ pr_located qs s @@ -836,7 +836,8 @@ module Make ) | VernacConstraint v -> let pr_uconstraint (l, d, r) = - pr_lident l ++ spc () ++ Univ.pr_constraint_type d ++ spc () ++ pr_lident r + pr_glob_level l ++ spc () ++ Univ.pr_constraint_type d ++ spc () ++ + pr_glob_level r in return ( hov 2 (keyword "Constraint" ++ spc () ++ @@ -1000,13 +1001,13 @@ module Make ) | VernacHints (_, dbnames,h) -> return (pr_hints dbnames h pr_constr pr_constr_pattern_expr) - | VernacSyntacticDefinition (id,(ids,c),_,onlyparsing) -> + | VernacSyntacticDefinition (id,(ids,c),_,compat) -> return ( hov 2 (keyword "Notation" ++ spc () ++ pr_lident id ++ spc () ++ prlist_with_sep spc pr_id ids ++ str":=" ++ pr_constrarg c ++ pr_syntax_modifiers - (match onlyparsing with None -> [] | Some v -> [SetOnlyParsing v])) + (match compat with None -> [] | Some v -> [SetCompatVersion v])) ) | VernacDeclareImplicits (q,[]) -> return ( @@ -1027,16 +1028,18 @@ module Make pr_smart_global q ++ let pr_s = function None -> str"" | Some (_,s) -> str "%" ++ str s in let pr_if b x = if b then x else str "" in - let pr_br imp max x = match imp, max with - | true, false -> str "[" ++ x ++ str "]" - | true, true -> str "{" ++ x ++ str "}" - | _ -> x in + let pr_br imp x = match imp with + | `Implicit -> str "[" ++ x ++ str "]" + | `MaximallyImplicit -> str "{" ++ x ++ str "}" + | `NotImplicit -> x in let rec aux n l = match n, l with | 0, l -> spc () ++ str"/" ++ aux ~-1 l | _, [] -> mt() - | n, (id,k,s,imp,max) :: tl -> - spc() ++ pr_br imp max (pr_if k (str"!") ++ pr_name id ++ pr_s s) ++ + | n, { name = id; recarg_like = k; + notation_scope = s; + implicit_status = imp } :: tl -> + spc() ++ pr_br imp (pr_if k (str"!") ++ pr_name id ++ pr_s s) ++ aux (n-1) tl in prlist_with_sep (fun () -> str", ") (aux nargs) impl ++ (if not (List.is_empty mods) then str" : " else str"") ++ |