interp_qed_delayed_proof doesn't need library internalization

lib/system.ml

@@ -313,6 +313,8 @@ let output_int64 ch n =
 type time = {real: float; user: float; system: float; }
 type duration = time
 
+let empty_duration = { real = 0.; user = 0.; system = 0. }
+
 let get_time () =
   let t = Unix.times ()  in
   { real = Unix.gettimeofday();

lib/system.mli

@@ -121,6 +121,8 @@ val check_caml_version : caml:string -> file:string -> unit
 type time
 type duration
 
+val empty_duration : duration
+
 val get_time : unit -> time
 val time_difference : time -> time -> float (** in seconds *)
 

vernac/synterp.ml

@@ -409,9 +409,19 @@ let with_succeed f =
   Vernacstate.Synterp.unfreeze st;
   ControlSucceed { st = transient_st } :: ctrl, v
 
+let synpure_control : control_flag -> control_entry =
+  let freeze = Vernacstate.Synterp.freeze in function
+  | ControlTime -> ControlTime { synterp_duration = System.empty_duration }
+  | ControlInstructions -> ControlInstructions { synterp_instructions = Ok 0L }
+  | ControlRedirect s -> ControlRedirect s
+  | ControlTimeout timeout ->
+    check_timeout timeout;
+    ControlTimeout { remaining = float_of_int timeout }
+  | ControlFail -> ControlFail { st = freeze() }
+  | ControlSucceed -> ControlSucceed { st = freeze() }
+
 (* We restore the state always *)
-let rec synterp_control_flag ~loc (f : control_flag list)
-    (fn : vernac_expr -> vernac_entry) expr =
+let rec synterp_control_flag ~loc (f : control_flag list) fn expr =
   match f with
   | [] -> [], fn expr
   | ControlFail :: l ->
@@ -562,15 +572,17 @@ let has_timeout ctrl = ctrl |> List.exists (function
     | Vernacexpr.ControlTimeout _ -> true
     | _ -> false)
 
-let synterp_control ~intern CAst.{ loc; v = cmd } =
-  let control = cmd.control in
-  let control = match !default_timeout with
-    | None -> control
-    | Some n ->
-      if has_timeout control then control
-      else Vernacexpr.ControlTimeout n :: control
-  in
-  synterp_control ~intern @@ CAst.make ?loc { cmd with control }
+let add_default_timeout control =
+  match !default_timeout with
+  | None -> control
+  | Some n ->
+    if has_timeout control then control
+    else Vernacexpr.ControlTimeout n :: control
+
+let synterp_control ~intern cmd =
+  synterp_control ~intern (CAst.map (fun cmd ->
+      { cmd with control = add_default_timeout cmd.control })
+      cmd)
 
 let synterp_control ~intern cmd =
   Flags.with_option Flags.in_synterp_phase (synterp_control ~intern) cmd

vernac/synterp.mli

@@ -35,6 +35,8 @@ type control_entry =
   | ControlFail of { st : Vernacstate.Synterp.t }
   | ControlSucceed of { st : Vernacstate.Synterp.t }
 
+(** Interprete control flag assuming a synpure command. *)
+val synpure_control : Vernacexpr.control_flag -> control_entry
 
 type synterp_entry =
   | EVernacNoop
@@ -87,6 +89,8 @@ val synterp_control :
   Vernacexpr.vernac_control ->
   vernac_control_entry
 
+val add_default_timeout : Vernacexpr.control_flag list -> Vernacexpr.control_flag list
+
 (** Default proof mode set by `start_proof` *)
 val get_default_proof_mode : unit -> Pvernac.proof_mode
 val proof_mode_opt_name : string list

vernac/vernacinterp.ml

@@ -224,9 +224,8 @@ let fs_intern dp =
 
 let interp_qed_delayed_proof ~proof ~st ~control (CAst.{loc; v = pe } as e) : Vernacstate.Interp.t =
   (* Synterp duplication of control handling bites us here... *)
-  let cmd = CAst.make ?loc { control; expr = VernacSynPure (VernacEndProof pe); attrs = [] } in
-  let CAst.{ loc; v = entry } = Synterp.synterp_control ~intern:fs_intern cmd in
-  let control = entry.control in
+  let control = Synterp.add_default_timeout control in
+  let control = List.map Synterp.synpure_control control in
   NewProfile.profile "interp-delayed-qed" (fun () ->
       interp_gen ~verbosely:false ~st
         ~interp_fn:(interp_qed_delayed_control ~proof ~control) e)