aboutsummaryrefslogtreecommitdiff
path: root/printing/ppvernac.ml
diff options
context:
space:
mode:
Diffstat (limited to 'printing/ppvernac.ml')
-rw-r--r--printing/ppvernac.ml136
1 files changed, 69 insertions, 67 deletions
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index 572876e5bf..415d703162 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -177,7 +177,7 @@ let pr_reference_or_constr pr_c = function
| HintsReference r -> pr_reference r
| HintsConstr c -> pr_c c
-let pr_hints local db h pr_c pr_pat =
+let pr_hints db h pr_c pr_pat =
let opth = pr_opt_hintbases db in
let pph =
match h with
@@ -200,7 +200,7 @@ let pr_hints local db h pr_c pr_pat =
str "Extern" ++ spc() ++ int n ++ spc() ++ pat ++ str" =>" ++
spc() ++ pr_raw_tactic tac
in
- hov 2 (str"Hint "++pr_locality local ++ pph ++ opth)
+ hov 2 (str"Hint "++ pph ++ opth)
let pr_with_declaration pr_c = function
| CWith_Definition (id,c) ->
@@ -306,7 +306,9 @@ let pr_class_rawexpr = function
| SortClass -> str"Sortclass"
| RefClass qid -> pr_smart_global qid
-let pr_assumption_token many = function
+let pr_assumption_token many (l,a) =
+ let l = match l with Some x -> x | None -> Decl_kinds.Global in
+ match l, a with
| (Discharge,Logical) ->
str (if many then "Hypotheses" else "Hypothesis")
| (Discharge,Definitional) ->
@@ -475,6 +477,8 @@ let pr_printable = function
in
let rec pr_vernac = function
+ | VernacProgram v -> str"Program" ++ spc() ++ pr_vernac v
+ | VernacLocal (local, v) -> pr_locality local ++ spc() ++ pr_vernac v
(* Proof management *)
| VernacAbortAll -> str "Abort All"
@@ -530,10 +534,9 @@ let rec pr_vernac = function
| VernacFail v -> str"Fail" ++ spc() ++ pr_vernac v
(* Syntax *)
- | VernacTacticNotation (local,n,r,e) ->
- pr_locality local ++ pr_grammar_tactic_rule n ("",r,e)
- | VernacOpenCloseScope (local,opening,sc) ->
- pr_section_locality local ++
+ | VernacTacticNotation (n,r,e) ->
+ pr_grammar_tactic_rule n ("",r,e)
+ | VernacOpenCloseScope (_,(opening,sc)) ->
str (if opening then "Open " else "Close ") ++
str "Scope" ++ spc() ++ str sc
| VernacDelimiters (sc,key) ->
@@ -542,20 +545,20 @@ let rec pr_vernac = function
| VernacBindScope (sc,cll) ->
str"Bind Scope" ++ spc () ++ str sc ++
spc() ++ str "with " ++ prlist_with_sep spc pr_smart_global cll
- | VernacArgumentsScope (local,q,scl) -> let pr_opt_scope = function
+ | VernacArgumentsScope (q,scl) -> let pr_opt_scope = function
| None -> str"_"
| Some sc -> str sc in
- pr_section_locality local ++ str"Arguments Scope" ++ spc() ++
+ str"Arguments Scope" ++ spc() ++
pr_smart_global q
++ spc() ++ str"[" ++ prlist_with_sep sep pr_opt_scope scl ++ str"]"
- | VernacInfix (local,((_,s),mv),q,sn) -> (* A Verifier *)
- hov 0 (hov 0 (pr_locality local ++ str"Infix "
+ | VernacInfix (_,((_,s),mv),q,sn) -> (* A Verifier *)
+ hov 0 (hov 0 (str"Infix "
++ qs s ++ str " :=" ++ pr_constrarg q) ++
pr_syntax_modifiers mv ++
(match sn with
| None -> mt()
| Some sc -> spc() ++ str":" ++ spc() ++ str sc))
- | VernacNotation (local,c,((_,s),l),opt) ->
+ | VernacNotation (_,c,((_,s),l),opt) ->
let ps =
let n = String.length s in
if n > 2 && s.[0] == '\'' && s.[n-1] == '\''
@@ -563,18 +566,20 @@ let rec pr_vernac = function
let s' = String.sub s 1 (n-2) in
if String.contains s' '\'' then qs s else str s'
else qs s in
- hov 2 (pr_locality local ++ str"Notation" ++ spc() ++ ps ++
+ hov 2 (str"Notation" ++ spc() ++ ps ++
str " :=" ++ pr_constrarg c ++ pr_syntax_modifiers l ++
(match opt with
| None -> mt()
| Some sc -> str" :" ++ spc() ++ str sc))
- | VernacSyntaxExtension (local,(s,l)) ->
- pr_locality local ++ str"Reserved Notation" ++ spc() ++ pr_located qs s ++
+ | VernacSyntaxExtension (_,(s,l)) ->
+ str"Reserved Notation" ++ spc() ++ pr_located qs s ++
pr_syntax_modifiers l
(* Gallina *)
| VernacDefinition (d,id,b) -> (* A verifier... *)
- let pr_def_token dk = str (Kindops.string_of_definition_kind dk) in
+ let pr_def_token (l,dk) =
+ let l = match l with Some x -> x | None -> Decl_kinds.Global in
+ str (Kindops.string_of_definition_kind (l,dk)) in
let pr_reduce = function
| None -> mt()
| Some r ->
@@ -650,9 +655,9 @@ let rec pr_vernac = function
| VernacFixpoint (local, recs) ->
let local = match local with
- | Discharge -> "Let "
- | Local -> "Local "
- | Global -> ""
+ | Some Discharge -> "Let "
+ | Some Local -> "Local "
+ | None | Some Global -> ""
in
let pr_onerec = function
| ((loc,id),ro,bl,type_,def),ntn ->
@@ -667,9 +672,9 @@ let rec pr_vernac = function
| VernacCoFixpoint (local, corecs) ->
let local = match local with
- | Discharge -> "Let "
- | Local -> "Local "
- | Global -> ""
+ | Some Discharge -> "Let "
+ | Some Local -> "Local "
+ | None | Some Global -> ""
in
let pr_onecorec (((loc,id),bl,c,def),ntn) =
pr_id id ++ spc() ++ pr_binders bl ++ spc() ++ str":" ++
@@ -698,22 +703,19 @@ let rec pr_vernac = function
(if f then str"Export" else str"Import") ++ spc() ++
prlist_with_sep sep pr_import_module l
| VernacCanonical q -> str"Canonical Structure" ++ spc() ++ pr_smart_global q
- | VernacCoercion (s,id,c1,c2) ->
+ | VernacCoercion (_,id,c1,c2) ->
hov 1 (
- str"Coercion" ++ (if s then spc() ++
- str"Local" ++ spc() else spc()) ++
+ str"Coercion" ++
pr_smart_global id ++ spc() ++ str":" ++ spc() ++ pr_class_rawexpr c1 ++
spc() ++ str">->" ++ spc() ++ pr_class_rawexpr c2)
- | VernacIdentityCoercion (s,id,c1,c2) ->
+ | VernacIdentityCoercion (_,id,c1,c2) ->
hov 1 (
- str"Identity Coercion" ++ (if s then spc() ++
- str"Local" ++ spc() else spc()) ++ pr_lident id ++
+ str"Identity Coercion" ++ pr_lident id ++
spc() ++ str":" ++ spc() ++ pr_class_rawexpr c1 ++ spc() ++ str">->" ++
spc() ++ pr_class_rawexpr c2)
- | VernacInstance (abst,glob, sup, (instid, bk, cl), props, pri) ->
+ | VernacInstance (abst, sup, (instid, bk, cl), props, pri) ->
hov 1 (
- pr_non_locality (not glob) ++
(if abst then str"Declare " else mt ()) ++
str"Instance" ++
(match snd instid with Name id -> spc () ++ pr_lident (fst instid, id) ++ spc () |
@@ -730,10 +732,10 @@ let rec pr_vernac = function
str"Context" ++ spc () ++ pr_and_type_binders_arg l)
- | VernacDeclareInstances (glob, ids) ->
- hov 1 (pr_non_locality (not glob) ++
- str"Existing" ++ spc () ++ str(String.plural (List.length ids) "Instance") ++
- spc () ++ prlist_with_sep spc pr_reference ids)
+ | VernacDeclareInstances ids ->
+ hov 1 ( str"Existing" ++ spc () ++
+ str(String.plural (List.length ids) "Instance") ++
+ spc () ++ prlist_with_sep spc pr_reference ids)
| VernacDeclareClass id ->
hov 1 (str"Existing" ++ spc () ++ str"Class" ++ spc () ++ pr_reference id)
@@ -784,13 +786,12 @@ let rec pr_vernac = function
| VernacRemoveLoadPath s -> str"Remove LoadPath" ++ qs s
| VernacAddMLPath (fl,s) ->
str"Add" ++ (if fl then str" Rec " else spc()) ++ str"ML Path" ++ qs s
- | VernacDeclareMLModule (local, l) ->
- pr_locality local ++
+ | VernacDeclareMLModule (l) ->
hov 2 (str"Declare ML Module" ++ spc() ++ prlist_with_sep sep qs l)
| VernacChdir s -> str"Cd" ++ pr_opt qs s
(* Commands *)
- | VernacDeclareTacticDefinition (local,rc,l) ->
+ | VernacDeclareTacticDefinition (rc,l) ->
let pr_tac_body (id, redef, body) =
let idl, body =
match body with
@@ -803,34 +804,33 @@ let rec pr_vernac = function
pr_raw_tactic body
in
hov 1
- (pr_locality local ++ str "Ltac " ++
+ (str "Ltac " ++
prlist_with_sep (fun () -> fnl() ++ str"with ") pr_tac_body l)
- | VernacCreateHintDb (local,dbname,b) ->
- hov 1 (pr_locality local ++ str "Create HintDb " ++
+ | VernacCreateHintDb (dbname,b) ->
+ hov 1 (str "Create HintDb " ++
str dbname ++ (if b then str" discriminated" else mt ()))
- | VernacRemoveHints (local, dbnames, ids) ->
- hov 1 (pr_locality local ++ str "Remove Hints " ++
+ | VernacRemoveHints (dbnames, ids) ->
+ hov 1 (str "Remove Hints " ++
prlist_with_sep spc (fun r -> pr_id (coerce_reference_to_id r)) ids ++
pr_opt_hintbases dbnames)
- | VernacHints (local,dbnames,h) ->
- pr_hints local dbnames h pr_constr pr_constr_pattern_expr
- | VernacSyntacticDefinition (id,(ids,c),local,onlyparsing) ->
+ | VernacHints (_, dbnames,h) ->
+ pr_hints dbnames h pr_constr pr_constr_pattern_expr
+ | VernacSyntacticDefinition (id,(ids,c),_,onlyparsing) ->
hov 2
- (pr_locality local ++ str"Notation " ++ pr_lident id ++ spc () ++
+ (str"Notation " ++ pr_lident id ++ spc () ++
prlist (fun x -> spc() ++ pr_id x) ids ++ str":=" ++ pr_constrarg c ++
pr_syntax_modifiers
(match onlyparsing with None -> [] | Some v -> [SetOnlyParsing v]))
- | VernacDeclareImplicits (local,q,[]) ->
- hov 2 (pr_section_locality local ++ str"Implicit Arguments" ++ spc() ++
- pr_smart_global q)
- | VernacDeclareImplicits (local,q,impls) ->
- hov 1 (pr_section_locality local ++ str"Implicit Arguments " ++
+ | VernacDeclareImplicits (q,[]) ->
+ hov 2 (str"Implicit Arguments" ++ spc() ++ pr_smart_global q)
+ | VernacDeclareImplicits (q,impls) ->
+ hov 1 (str"Implicit Arguments " ++
spc() ++ pr_smart_global q ++ spc() ++
prlist_with_sep spc (fun imps ->
str"[" ++ prlist_with_sep sep pr_explanation imps ++ str"]")
impls)
- | VernacArguments (local, q, impl, nargs, mods) ->
- hov 2 (pr_section_locality local ++ str"Arguments" ++ spc() ++
+ | VernacArguments (q, impl, nargs, mods) ->
+ hov 2 (str"Arguments" ++ spc() ++
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
@@ -861,21 +861,23 @@ let rec pr_vernac = function
hov 2 (str"Implicit Type" ++
str (if n > 1 then "s " else " ") ++
pr_ne_params_list pr_lconstr_expr (List.map (fun sb -> false,sb) bl))
- | VernacGeneralizable (local, g) ->
- hov 1 (pr_locality local ++ str"Generalizable Variable" ++
+ | VernacGeneralizable g ->
+ hov 1 (str"Generalizable Variable" ++
match g with
| None -> str "s none"
| Some [] -> str "s all"
| Some idl ->
str (if List.length idl > 1 then "s " else " ") ++
prlist_with_sep spc pr_lident idl)
- | VernacSetOpacity(b,[k,l]) when Conv_oracle.is_transparent k ->
- hov 1 (pr_non_locality b ++ str "Transparent" ++
+ | VernacSetOpacity(k,l) when Conv_oracle.is_transparent k ->
+ hov 1 (str "Transparent" ++
spc() ++ prlist_with_sep sep pr_smart_global l)
- | VernacSetOpacity(b,[Conv_oracle.Opaque,l]) ->
- hov 1 (pr_non_locality b ++ str "Opaque" ++
+ | VernacSetOpacity(Conv_oracle.Opaque,l) ->
+ hov 1 (str "Opaque" ++
spc() ++ prlist_with_sep sep pr_smart_global l)
- | VernacSetOpacity (local,l) ->
+ | VernacSetOpacity _ ->
+ Errors.anomaly (str "VernacSetOpacity used to set something else")
+ | VernacSetStrategy l ->
let pr_lev = function
Conv_oracle.Opaque -> str"opaque"
| Conv_oracle.Expand -> str"expand"
@@ -884,12 +886,12 @@ let rec pr_vernac = function
let pr_line (l,q) =
hov 2 (pr_lev l ++ spc() ++
str"[" ++ prlist_with_sep sep pr_smart_global q ++ str"]") in
- hov 1 (pr_locality local ++ str "Strategy" ++ spc() ++
+ hov 1 (str "Strategy" ++ spc() ++
hv 0 (prlist_with_sep sep pr_line l))
- | VernacUnsetOption (l,na) ->
- hov 1 (pr_locality_full l ++ str"Unset" ++ spc() ++ pr_printoption na None)
- | VernacSetOption (l,na,v) ->
- hov 2 (pr_locality_full l ++ str"Set" ++ spc() ++ pr_set_option na v)
+ | VernacUnsetOption (na) ->
+ hov 1 (str"Unset" ++ spc() ++ pr_printoption na None)
+ | VernacSetOption (na,v) ->
+ hov 2 (str"Set" ++ spc() ++ pr_set_option na v)
| VernacAddOption (na,l) -> hov 2 (str"Add" ++ spc() ++ pr_printoption na (Some l))
| VernacRemoveOption (na,l) -> hov 2 (str"Remove" ++ spc() ++ pr_printoption na (Some l))
| VernacMemOption (na,l) -> hov 2 (str"Test" ++ spc() ++ pr_printoption na (Some l))
@@ -905,8 +907,8 @@ let rec pr_vernac = function
let pr_i = match io with None -> mt () | Some i -> int i ++ str ": " in
pr_i ++ pr_mayeval r c
| VernacGlobalCheck c -> hov 2 (str"Type" ++ pr_constrarg c)
- | VernacDeclareReduction (b,s,r) ->
- pr_locality b ++ str "Declare Reduction " ++ str s ++ str " := " ++
+ | VernacDeclareReduction (s,r) ->
+ str "Declare Reduction " ++ str s ++ str " := " ++
pr_red_expr (pr_constr,pr_lconstr,pr_smart_global, pr_constr) r
| VernacPrint p -> pr_printable p
| VernacSearch (sea,sea_r) -> pr_search sea sea_r pr_constr_pattern_expr
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-25 21:56:10 +0000