[toplevel] Annotate tailcall functions

This will ensure that we don't introduce problems as it has happened
in the past.

While we are at it, we fix one easy case of non-tail call.

3 files changed, 10 insertions, 17 deletions

diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml
index 2c5faa4df7..79de3c86b6 100644
--- a/toplevel/coqloop.ml
+++ b/toplevel/coqloop.ml
@@ -499,7 +499,7 @@ let rec vernac_loop ~state =
   if !print_emacs then top_stderr (str (top_buffer.prompt state.doc));
   resynch_buffer top_buffer;
   let state, drop = read_and_execute ~state in
-  if drop then state else vernac_loop ~state
+  if drop then state else (vernac_loop [@ocaml.tailcall]) ~state
 
 (* Default toplevel loop, machinery for drop is below *)
 
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index c4c8492a4a..92e664d56b 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -110,7 +110,7 @@ let load_vernac_core ~echo ~check ~interactive ~state file =
       let state =
         Flags.silently (interp_vernac ~check ~interactive ~state) ast in
 
-      loop state (state.sid :: ids)
+      (loop [@ocaml.tailcall]) state (state.sid :: ids)
   in
   try loop state []
   with any ->   (* whatever the exception *)
diff --git a/vernac/vernacinterp.ml b/vernac/vernacinterp.ml
index 7d25e6b852..7ab21141df 100644
--- a/vernac/vernacinterp.ml
+++ b/vernac/vernacinterp.ml
@@ -166,8 +166,6 @@ let rec interp_expr ~atts ~st c =
     interp_typed_vernac ~stack fv
 
 and vernac_load ~verbosely fname =
-  let exception End_of_input in
-
   (* Note that no proof should be open here, so the state here is just token for now *)
   let st = Vernacstate.freeze_interp_state ~marshallable:false in
   let fname =
@@ -180,20 +178,15 @@ and vernac_load ~verbosely fname =
   (* Parsing loop *)
   let v_mod = if verbosely then Flags.verbosely else Flags.silently in
   let parse_sentence proof_mode = Flags.with_option Flags.we_are_parsing
-      (fun po ->
-         match Pcoq.Entry.parse (Pvernac.main_entry proof_mode) po with
-         | Some x -> x
-         | None -> raise End_of_input) in
+      (Pcoq.Entry.parse (Pvernac.main_entry proof_mode))
+  in
   let rec load_loop ~stack =
-    try
-      let proof_mode = Option.map (fun _ -> get_default_proof_mode ()) stack in
-      let stack =
-        v_mod (interp_control ~st:{ st with Vernacstate.lemmas = stack })
-          (parse_sentence proof_mode input) in
-      load_loop ~stack
-    with
-      End_of_input ->
-      stack
+    let proof_mode = Option.map (fun _ -> get_default_proof_mode ()) stack in
+    match parse_sentence proof_mode input with
+    | None -> stack
+    | Some stm ->
+      let stack = v_mod (interp_control ~st:{ st with Vernacstate.lemmas = stack }) stm in
+      (load_loop [@ocaml.tailcall]) ~stack
   in
   let stack = load_loop ~stack:st.Vernacstate.lemmas in
   (* If Load left a proof open, we fail too. *)