aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing/ppvernac.ml
diff options
context:
space:
mode:
Diffstat (limited to 'parsing/ppvernac.ml')
-rw-r--r--parsing/ppvernac.ml5
1 files changed, 5 insertions, 0 deletions
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml
index c74922351..6213e4fda 100644
--- a/parsing/ppvernac.ml
+++ b/parsing/ppvernac.ml
@@ -602,6 +602,11 @@ let rec pr_vernac = function
| VernacScheme l ->
hov 2 (str"Scheme" ++ spc() ++
prlist_with_sep (fun _ -> fnl() ++ str"with ") pr_onescheme l)
+ | VernacCombinedScheme (id, l) ->
+ hov 2 (str"Combined Scheme" ++ spc() ++
+ pr_lident id ++ spc() ++ str"from" ++ spc() ++
+ prlist_with_sep (fun _ -> fnl() ++ str", ") pr_lident l)
+
(* Gallina extensions *)
| VernacRecord (b,(oc,name),ps,s,c,fs) ->