aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rw-r--r--toplevel/vernac.ml3
1 files changed, 3 insertions, 0 deletions
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 888c3411d..6051b65a4 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -263,6 +263,9 @@ let rec vernac_com verbosely checknav (loc,com) =
raise reraise
end
+ | VernacList l ->
+ List.iter (fun (_,v) -> interp v) l
+
| v when !just_parsing -> ()
| v -> Stm.process_transaction verbosely (loc,v)