aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--.merlin2
-rw-r--r--Makefile.common8
-rw-r--r--proofs/proof_global.ml7
-rw-r--r--stm/stm.ml285
-rw-r--r--stm/stm.mli7
-rw-r--r--stm/stm.mllib1
-rw-r--r--tools/coq_makefile.ml2
-rw-r--r--tools/coqmktop.ml1
-rw-r--r--toplevel/toplevel.mllib16
-rw-r--r--toplevel/vernac.ml2
-rw-r--r--vernac/assumptions.ml (renamed from toplevel/assumptions.ml)0
-rw-r--r--vernac/assumptions.mli (renamed from toplevel/assumptions.mli)0
-rw-r--r--vernac/auto_ind_decl.ml (renamed from toplevel/auto_ind_decl.ml)0
-rw-r--r--vernac/auto_ind_decl.mli (renamed from toplevel/auto_ind_decl.mli)0
-rw-r--r--vernac/class.ml (renamed from toplevel/class.ml)0
-rw-r--r--vernac/class.mli (renamed from toplevel/class.mli)0
-rw-r--r--vernac/classes.ml (renamed from toplevel/classes.ml)0
-rw-r--r--vernac/classes.mli (renamed from toplevel/classes.mli)0
-rw-r--r--vernac/command.ml (renamed from toplevel/command.ml)0
-rw-r--r--vernac/command.mli (renamed from toplevel/command.mli)0
-rw-r--r--vernac/discharge.ml (renamed from toplevel/discharge.ml)0
-rw-r--r--vernac/discharge.mli (renamed from toplevel/discharge.mli)0
-rw-r--r--vernac/doc.tex (renamed from toplevel/doc.tex)0
-rw-r--r--vernac/explainErr.ml (renamed from toplevel/explainErr.ml)0
-rw-r--r--vernac/explainErr.mli (renamed from toplevel/explainErr.mli)0
-rw-r--r--vernac/himsg.ml (renamed from toplevel/himsg.ml)0
-rw-r--r--vernac/himsg.mli (renamed from toplevel/himsg.mli)0
-rw-r--r--vernac/ind_tables.ml (renamed from toplevel/ind_tables.ml)0
-rw-r--r--vernac/ind_tables.mli (renamed from toplevel/ind_tables.mli)0
-rw-r--r--vernac/indschemes.ml (renamed from toplevel/indschemes.ml)0
-rw-r--r--vernac/indschemes.mli (renamed from toplevel/indschemes.mli)0
-rw-r--r--vernac/lemmas.ml (renamed from stm/lemmas.ml)0
-rw-r--r--vernac/lemmas.mli (renamed from stm/lemmas.mli)0
-rw-r--r--vernac/locality.ml (renamed from toplevel/locality.ml)0
-rw-r--r--vernac/locality.mli (renamed from toplevel/locality.mli)0
-rw-r--r--vernac/metasyntax.ml (renamed from toplevel/metasyntax.ml)0
-rw-r--r--vernac/metasyntax.mli (renamed from toplevel/metasyntax.mli)0
-rw-r--r--vernac/mltop.ml (renamed from toplevel/mltop.ml)0
-rw-r--r--vernac/mltop.mli (renamed from toplevel/mltop.mli)0
-rw-r--r--vernac/obligations.ml (renamed from toplevel/obligations.ml)6
-rw-r--r--vernac/obligations.mli (renamed from toplevel/obligations.mli)6
-rw-r--r--vernac/record.ml (renamed from toplevel/record.ml)0
-rw-r--r--vernac/record.mli (renamed from toplevel/record.mli)0
-rw-r--r--vernac/search.ml (renamed from toplevel/search.ml)0
-rw-r--r--vernac/search.mli (renamed from toplevel/search.mli)0
-rw-r--r--vernac/vernac.mllib17
-rw-r--r--vernac/vernacentries.ml (renamed from toplevel/vernacentries.ml)70
-rw-r--r--vernac/vernacentries.mli (renamed from toplevel/vernacentries.mli)0
-rw-r--r--vernac/vernacinterp.ml (renamed from toplevel/vernacinterp.ml)0
-rw-r--r--vernac/vernacinterp.mli (renamed from toplevel/vernacinterp.mli)0
50 files changed, 226 insertions, 204 deletions
diff --git a/.merlin b/.merlin
index 7410e601b..bda18d549 100644
--- a/.merlin
+++ b/.merlin
@@ -34,6 +34,8 @@ S stm
B stm
S toplevel
B toplevel
+S vernac
+B vernac
S tools
B tools
diff --git a/Makefile.common b/Makefile.common
index 49fe1fd93..2cf4d0169 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -53,9 +53,9 @@ INSTALLSH:=./install.sh
MKDIR:=install -d
CORESRCDIRS:=\
- config lib kernel kernel/byterun library \
- proofs tactics pretyping interp stm \
- toplevel parsing printing intf engine ltac
+ config lib kernel intf kernel/byterun library \
+ engine pretyping interp proofs parsing printing \
+ tactics vernac stm toplevel ltac
PLUGINDIRS:=\
omega romega micromega quote \
@@ -83,7 +83,7 @@ BYTERUN:=$(addprefix kernel/byterun/, \
CORECMA:=lib/clib.cma lib/lib.cma kernel/kernel.cma library/library.cma \
engine/engine.cma pretyping/pretyping.cma interp/interp.cma proofs/proofs.cma \
- parsing/parsing.cma printing/printing.cma tactics/tactics.cma \
+ parsing/parsing.cma printing/printing.cma tactics/tactics.cma vernac/vernac.cma \
stm/stm.cma toplevel/toplevel.cma parsing/highparsing.cma ltac/ltac.cma
TOPLOOPCMA:=stm/proofworkertop.cma stm/tacworkertop.cma stm/queryworkertop.cma
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index a2ee62221..120cde5e5 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -317,7 +317,10 @@ let constrain_variables init uctx =
let cstrs = UState.constrain_variables levels uctx in
Univ.ContextSet.add_constraints cstrs (UState.context_set uctx)
-let close_proof ~keep_body_ucst_separate ?feedback_id ~now fpl =
+type closed_proof_output = (Term.constr * Safe_typing.private_constants) list * Evd.evar_universe_context
+
+let close_proof ~keep_body_ucst_separate ?feedback_id ~now
+ (fpl : closed_proof_output Future.computation) =
let { pid; section_vars; strength; proof; terminator; universe_binders } =
cur_pstate () in
let poly = pi2 strength (* Polymorphic *) in
@@ -395,8 +398,6 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now fpl =
universes = (universes, binders) },
fun pr_ending -> CEphemeron.get terminator pr_ending
-type closed_proof_output = (Term.constr * Safe_typing.private_constants) list * Evd.evar_universe_context
-
let return_proof ?(allow_partial=false) () =
let { pid; proof; strength = (_,poly,_) } = cur_pstate () in
if allow_partial then begin
diff --git a/stm/stm.ml b/stm/stm.ml
index 6f34c8dbc..e698d1c72 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -24,11 +24,13 @@ open Ppvernac
open Vernac_classifier
open Feedback
+let execution_error state_id loc msg =
+ feedback ~id:(State state_id)
+ (Message (Error, Some loc, pp_to_richpp msg))
+
module Hooks = struct
let process_error, process_error_hook = Hook.make ()
-let interp, interp_hook = Hook.make ()
-let with_fail, with_fail_hook = Hook.make ()
let state_computed, state_computed_hook = Hook.make
~default:(fun state_id ~in_cache ->
@@ -48,10 +50,6 @@ let parse_error, parse_error_hook = Hook.make
~default:(fun id loc msg ->
feedback ~id (Message(Error, Some loc, pp_to_richpp msg))) ()
-let execution_error, execution_error_hook = Hook.make
- ~default:(fun state_id loc msg ->
- feedback ~id:(State state_id) (Message(Error, Some loc, pp_to_richpp msg))) ()
-
let unreachable_state, unreachable_state_hook = Hook.make
~default:(fun _ _ -> ()) ()
@@ -105,26 +103,6 @@ let may_pierce_opaque = function
| { expr = VernacExtend (("ExtractionInductive",_), _) } -> true
| _ -> false
-(* Wrapper for Vernacentries.interp to set the feedback id *)
-let vernac_interp ?proof id ?route { verbose; loc; expr } =
- let rec internal_command = function
- | VernacResetName _ | VernacResetInitial | VernacBack _
- | VernacBackTo _ | VernacRestart | VernacUndo _ | VernacUndoTo _
- | VernacBacktrack _ | VernacAbortAll | VernacAbort _ -> true
- | VernacTime (_,e) | VernacTimeout (_,e) | VernacRedirect (_,(_,e)) -> internal_command e
- | _ -> false in
- if internal_command expr then begin
- prerr_endline (fun () -> "ignoring " ^ Pp.string_of_ppcmds(pr_vernac expr))
- end else begin
- set_id_for_feedback ?route (State id);
- Aux_file.record_in_aux_set_at loc;
- prerr_endline (fun () -> "interpreting " ^ Pp.string_of_ppcmds(pr_vernac expr));
- try Hooks.(call interp ?verbosely:(Some verbose) ?proof (loc, expr))
- with e ->
- let e = CErrors.push e in
- iraise Hooks.(call_process_error_once e)
- end
-
(* Wrapper for Vernac.parse_sentence to set the feedback id *)
let indentation_of_string s =
let len = String.length s in
@@ -860,7 +838,7 @@ end = struct (* {{{ *)
| None ->
let loc = Option.default Loc.ghost (Loc.get_loc info) in
let (e, info) = Hooks.(call_process_error_once (e, info)) in
- Hooks.(call execution_error id loc (iprint (e, info)));
+ execution_error id loc (iprint (e, info));
(e, Stateid.add info ~valid id)
let same_env { system = s1 } { system = s2 } =
@@ -910,6 +888,126 @@ end = struct (* {{{ *)
end (* }}} *)
+(* indentation code for Show Script, initially contributed
+ * by D. de Rauglaudre. Should be moved away.
+ *)
+
+module ShowScript = struct
+
+let indent_script_item ((ng1,ngl1),nl,beginend,ppl) (cmd,ng) =
+ (* ng1 : number of goals remaining at the current level (before cmd)
+ ngl1 : stack of previous levels with their remaining goals
+ ng : number of goals after the execution of cmd
+ beginend : special indentation stack for { } *)
+ let ngprev = List.fold_left (+) ng1 ngl1 in
+ let new_ngl =
+ if ng > ngprev then
+ (* We've branched *)
+ (ng - ngprev + 1, ng1 - 1 :: ngl1)
+ else if ng < ngprev then
+ (* A subgoal have been solved. Let's compute the new current level
+ by discarding all levels with 0 remaining goals. *)
+ let rec loop = function
+ | (0, ng2::ngl2) -> loop (ng2,ngl2)
+ | p -> p
+ in loop (ng1-1, ngl1)
+ else
+ (* Standard case, same goal number as before *)
+ (ng1, ngl1)
+ in
+ (* When a subgoal have been solved, separate this block by an empty line *)
+ let new_nl = (ng < ngprev)
+ in
+ (* Indentation depth *)
+ let ind = List.length ngl1
+ in
+ (* Some special handling of bullets and { }, to get a nicer display *)
+ let pred n = max 0 (n-1) in
+ let ind, nl, new_beginend = match cmd with
+ | VernacSubproof _ -> pred ind, nl, (pred ind)::beginend
+ | VernacEndSubproof -> List.hd beginend, false, List.tl beginend
+ | VernacBullet _ -> pred ind, nl, beginend
+ | _ -> ind, nl, beginend
+ in
+ let pp =
+ (if nl then fnl () else mt ()) ++
+ (hov (ind+1) (str (String.make ind ' ') ++ Ppvernac.pr_vernac cmd))
+ in
+ (new_ngl, new_nl, new_beginend, pp :: ppl)
+
+let get_script prf =
+ let branch, test =
+ match prf with
+ | None -> VCS.Branch.master, fun _ -> true
+ | Some name -> VCS.current_branch (),fun nl -> nl=[] || List.mem name nl in
+ let rec find acc id =
+ if Stateid.equal id Stateid.initial ||
+ Stateid.equal id Stateid.dummy then acc else
+ let view = VCS.visit id in
+ match view.step with
+ | `Fork((_,_,_,ns), _) when test ns -> acc
+ | `Qed (qed, proof) -> find [qed.qast.expr, (VCS.get_info id).n_goals] proof
+ | `Sideff (`Ast (x,_)) ->
+ find ((x.expr, (VCS.get_info id).n_goals)::acc) view.next
+ | `Sideff (`Id id) -> find acc id
+ | `Cmd {cast = x; ctac} when ctac -> (* skip non-tactics *)
+ find ((x.expr, (VCS.get_info id).n_goals)::acc) view.next
+ | `Cmd _ -> find acc view.next
+ | `Alias (id,_) -> find acc id
+ | `Fork _ -> find acc view.next
+ in
+ find [] (VCS.get_branch_pos branch)
+
+let show_script ?proof () =
+ try
+ let prf =
+ try match proof with
+ | None -> Some (Pfedit.get_current_proof_name ())
+ | Some (p,_) -> Some (p.Proof_global.id)
+ with Proof_global.NoCurrentProof -> None
+ in
+ let cmds = get_script prf in
+ let _,_,_,indented_cmds =
+ List.fold_left indent_script_item ((1,[]),false,[],[]) cmds
+ in
+ let indented_cmds = List.rev (indented_cmds) in
+ msg_notice (v 0 (prlist_with_sep fnl (fun x -> x) indented_cmds))
+ with Vcs_aux.Expired -> ()
+
+end
+
+(* Wrapper for Vernacentries.interp to set the feedback id *)
+(* It is currently called 19 times, this number should be certainly
+ reduced... *)
+let stm_vernac_interp ?proof id ?route { verbose; loc; expr } =
+ (* The Stm will gain the capability to interpret commmads affecting
+ the whole document state, such as backtrack, etc... so we start
+ to design the stm command interpreter now *)
+ set_id_for_feedback ?route (State id);
+ Aux_file.record_in_aux_set_at loc;
+ (* We need to check if a command should be filtered from
+ * vernac_entries, as it cannot handle it. This should go away in
+ * future refactorings.
+ *)
+ let rec is_filtered_command = function
+ | VernacResetName _ | VernacResetInitial | VernacBack _
+ | VernacBackTo _ | VernacRestart | VernacUndo _ | VernacUndoTo _
+ | VernacBacktrack _ | VernacAbortAll | VernacAbort _ -> true
+ | VernacTime (_,e) | VernacTimeout (_,e) | VernacRedirect (_,(_,e)) -> is_filtered_command e
+ | _ -> false
+ in
+ let aux_interp cmd =
+ if is_filtered_command cmd then
+ prerr_endline (fun () -> "ignoring " ^ Pp.string_of_ppcmds(pr_vernac expr))
+ else match cmd with
+ | VernacShow ShowScript -> ShowScript.show_script ()
+ | expr ->
+ prerr_endline (fun () -> "interpreting " ^ Pp.string_of_ppcmds(pr_vernac expr));
+ try Vernacentries.interp ?verbosely:(Some verbose) ?proof (loc, expr)
+ with e ->
+ let e = CErrors.push e in
+ iraise Hooks.(call_process_error_once e)
+ in aux_interp expr
(****************************** CRUFT *****************************************)
(******************************************************************************)
@@ -1287,7 +1385,7 @@ end = struct (* {{{ *)
let info = Stateid.add ~valid:start Exninfo.null start in
let e = (RemoteException (strbrk s), info) in
t_assign (`Exn e);
- Hooks.(call execution_error start Loc.ghost (strbrk s));
+ execution_error start Loc.ghost (strbrk s);
feedback (InProgress ~-1)
let build_proof_here ~drop_pt (id,valid) loc eop =
@@ -1321,7 +1419,7 @@ end = struct (* {{{ *)
Proof_global.close_future_proof stop (Future.from_val ~fix_exn p) in
let terminator = (* The one sent by master is an InvalidKey *)
Lemmas.(standard_proof_terminator [] (mk_hook (fun _ _ -> ()))) in
- vernac_interp stop
+ stm_vernac_interp stop
~proof:(pobject, terminator)
{ verbose = false; loc; indentation = 0; strlen = 0;
expr = (VernacEndProof (Proved (Opaque None,None))) }) in
@@ -1463,7 +1561,7 @@ end = struct (* {{{ *)
(* We jump at the beginning since the kernel handles side effects by also
* looking at the ones that happen to be present in the current env *)
Reach.known_state ~cache:`No start;
- vernac_interp stop ~proof
+ stm_vernac_interp stop ~proof
{ verbose = false; loc; indentation = 0; strlen = 0;
expr = (VernacEndProof (Proved (Opaque None,None))) };
`OK proof
@@ -1714,7 +1812,7 @@ end = struct (* {{{ *)
else begin
let (i, ast) = r_ast in
Proof_global.simple_with_current_proof (fun _ p -> Proof.focus focus_cond () i p);
- vernac_interp r_state_fb ast;
+ stm_vernac_interp r_state_fb ast;
let _,_,_,_,sigma = Proof.proof (Proof_global.give_me_the_proof ()) in
match Evd.(evar_body (find sigma r_goal)) with
| Evd.Evar_empty -> RespNoProgress
@@ -1750,7 +1848,7 @@ end = struct (* {{{ *)
| VernacTime (_,e) | VernacRedirect (_,(_,e)) -> find true fail e
| VernacFail e -> find time true e
| _ -> e, time, fail in find false false e in
- Hooks.call Hooks.with_fail fail (fun () ->
+ Vernacentries.with_fail fail (fun () ->
(if time then System.with_time false else (fun x -> x)) (fun () ->
ignore(TaskQueue.with_n_workers nworkers (fun queue ->
Proof_global.with_current_proof (fun _ p ->
@@ -1843,7 +1941,7 @@ end = struct (* {{{ *)
VCS.print ();
Reach.known_state ~cache:`No r_where;
try
- vernac_interp r_for { r_what with verbose = true };
+ stm_vernac_interp r_for { r_what with verbose = true };
feedback ~id:(State r_for) Processed
with e when CErrors.noncritical e ->
let e = CErrors.push e in
@@ -2052,7 +2150,7 @@ let known_state ?(redefine_qed=false) ~cache id =
Proof_global.with_current_proof (fun _ p ->
feedback ~id:(State id) Feedback.AddedAxiom;
fst (Pfedit.solve Vernacexpr.SelectAll None tac p), ());
- Option.iter (fun expr -> vernac_interp id {
+ Option.iter (fun expr -> stm_vernac_interp id {
verbose = true; loc = Loc.ghost; expr; indentation = 0;
strlen = 0 })
recovery_command
@@ -2131,24 +2229,24 @@ let known_state ?(redefine_qed=false) ~cache id =
resilient_tactic id cblock (fun () ->
reach view.next;
Hooks.(call tactic_being_run true);
- vernac_interp id x;
+ stm_vernac_interp id x;
Hooks.(call tactic_being_run false));
if eff then update_global_env ()
), (if eff then `Yes else cache), true
| `Cmd { cast = x; ceff = eff } -> (fun () ->
resilient_command reach view.next;
- vernac_interp id x;
+ stm_vernac_interp id x;
if eff then update_global_env ()
), (if eff then `Yes else cache), true
| `Fork ((x,_,_,_), None) -> (fun () ->
resilient_command reach view.next;
- vernac_interp id x;
+ stm_vernac_interp id x;
wall_clock_last_fork := Unix.gettimeofday ()
), `Yes, true
| `Fork ((x,_,_,_), Some prev) -> (fun () -> (* nested proof *)
reach ~cache:`Shallow prev;
reach view.next;
- (try vernac_interp id x;
+ (try stm_vernac_interp id x;
with e when CErrors.noncritical e ->
let (e, info) = CErrors.push e in
let info = Stateid.add info ~valid:prev id in
@@ -2198,14 +2296,14 @@ let known_state ?(redefine_qed=false) ~cache id =
Proof_global.close_future_proof ~feedback_id:id fp in
if not delegate then ignore(Future.compute fp);
reach view.next;
- vernac_interp id ~proof x;
+ stm_vernac_interp id ~proof x;
feedback ~id:(State id) Incomplete
| { VCS.kind = `Master }, _ -> assert false
end;
Proof_global.discard_all ()
), (if redefine_qed then `No else `Yes), true
| `Sync (name, _, `Immediate) -> (fun () ->
- reach eop; vernac_interp id x; Proof_global.discard_all ()
+ reach eop; stm_vernac_interp id x; Proof_global.discard_all ()
), `Yes, true
| `Sync (name, pua, reason) -> (fun () ->
log_processing_sync id name reason;
@@ -2226,7 +2324,7 @@ let known_state ?(redefine_qed=false) ~cache id =
if keep != VtKeepAsAxiom then
reach view.next;
let wall_clock2 = Unix.gettimeofday () in
- vernac_interp id ?proof x;
+ stm_vernac_interp id ?proof x;
let wall_clock3 = Unix.gettimeofday () in
Aux_file.record_in_aux_at x.loc "proof_check_time"
(Printf.sprintf "%.3f" (wall_clock3 -. wall_clock2));
@@ -2242,7 +2340,7 @@ let known_state ?(redefine_qed=false) ~cache id =
in
aux (collect_proof keep (view.next, x) brname brinfo eop)
| `Sideff (`Ast (x,_)) -> (fun () ->
- reach view.next; vernac_interp id x; update_global_env ()
+ reach view.next; stm_vernac_interp id x; update_global_env ()
), cache, true
| `Sideff (`Id origin) -> (fun () ->
reach view.next;
@@ -2430,7 +2528,7 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty
" classified as: " ^ string_of_vernac_classification c);
match c with
(* PG stuff *)
- | VtStm(VtPG,false), VtNow -> vernac_interp Stateid.dummy x; `Ok
+ | VtStm(VtPG,false), VtNow -> stm_vernac_interp Stateid.dummy x; `Ok
| VtStm(VtPG,_), _ -> anomaly(str "PG command in script or VtLater")
(* Joining various parts of the document *)
| VtStm (VtJoinDocument, b), VtNow -> join (); `Ok
@@ -2474,13 +2572,13 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty
(* Query *)
| VtQuery (false,(report_id,route)), VtNow when tty = true ->
finish ();
- (try Future.purify (vernac_interp report_id ~route)
+ (try Future.purify (stm_vernac_interp report_id ~route)
{x with verbose = true }
with e when CErrors.noncritical e ->
let e = CErrors.push e in
iraise (State.exn_on ~valid:Stateid.dummy report_id e)); `Ok
| VtQuery (false,(report_id,route)), VtNow ->
- (try vernac_interp report_id ~route x
+ (try stm_vernac_interp report_id ~route x
with e ->
let e = CErrors.push e in
iraise (State.exn_on ~valid:Stateid.dummy report_id e)); `Ok
@@ -2553,7 +2651,7 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty
(* Side effect on all branches *)
| VtUnknown, _ when expr = VernacToplevelControl Drop ->
- vernac_interp (VCS.get_branch_pos head) x; `Ok
+ stm_vernac_interp (VCS.get_branch_pos head) x; `Ok
| VtSideff l, w ->
let in_proof = not (VCS.Branch.equal head VCS.Branch.master) in
@@ -2579,7 +2677,7 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty
VCS.checkout VCS.Branch.master;
let mid = VCS.get_branch_pos VCS.Branch.master in
Reach.known_state ~cache:(interactive ()) mid;
- vernac_interp id x;
+ stm_vernac_interp id x;
(* Vernac x may or may not start a proof *)
if not in_proof && Proof_global.there_are_pending_proofs () then
begin
@@ -2609,7 +2707,7 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty
begin match expr with
| VernacStm (PGLast _) ->
if not (VCS.Branch.equal head VCS.Branch.master) then
- vernac_interp Stateid.dummy
+ stm_vernac_interp Stateid.dummy
{ verbose = true; loc = Loc.ghost; indentation = 0; strlen = 0;
expr = VernacShow (ShowGoal OpenSubgoals) }
| _ -> ()
@@ -2856,102 +2954,13 @@ let proofname b = match VCS.get_branch b with
let get_all_proof_names () =
List.map unmangle (List.map_filter proofname (VCS.branches ()))
-let get_current_proof_name () =
- Option.map unmangle (proofname (VCS.current_branch ()))
-
-let get_script prf =
- let branch, test =
- match prf with
- | None -> VCS.Branch.master, fun _ -> true
- | Some name -> VCS.current_branch (),fun nl -> nl=[] || List.mem name nl in
- let rec find acc id =
- if Stateid.equal id Stateid.initial ||
- Stateid.equal id Stateid.dummy then acc else
- let view = VCS.visit id in
- match view.step with
- | `Fork((_,_,_,ns), _) when test ns -> acc
- | `Qed (qed, proof) -> find [qed.qast.expr, (VCS.get_info id).n_goals] proof
- | `Sideff (`Ast (x,_)) ->
- find ((x.expr, (VCS.get_info id).n_goals)::acc) view.next
- | `Sideff (`Id id) -> find acc id
- | `Cmd {cast = x; ctac} when ctac -> (* skip non-tactics *)
- find ((x.expr, (VCS.get_info id).n_goals)::acc) view.next
- | `Cmd _ -> find acc view.next
- | `Alias (id,_) -> find acc id
- | `Fork _ -> find acc view.next
- in
- find [] (VCS.get_branch_pos branch)
-
-(* indentation code for Show Script, initially contributed
- by D. de Rauglaudre *)
-
-let indent_script_item ((ng1,ngl1),nl,beginend,ppl) (cmd,ng) =
- (* ng1 : number of goals remaining at the current level (before cmd)
- ngl1 : stack of previous levels with their remaining goals
- ng : number of goals after the execution of cmd
- beginend : special indentation stack for { } *)
- let ngprev = List.fold_left (+) ng1 ngl1 in
- let new_ngl =
- if ng > ngprev then
- (* We've branched *)
- (ng - ngprev + 1, ng1 - 1 :: ngl1)
- else if ng < ngprev then
- (* A subgoal have been solved. Let's compute the new current level
- by discarding all levels with 0 remaining goals. *)
- let rec loop = function
- | (0, ng2::ngl2) -> loop (ng2,ngl2)
- | p -> p
- in loop (ng1-1, ngl1)
- else
- (* Standard case, same goal number as before *)
- (ng1, ngl1)
- in
- (* When a subgoal have been solved, separate this block by an empty line *)
- let new_nl = (ng < ngprev)
- in
- (* Indentation depth *)
- let ind = List.length ngl1
- in
- (* Some special handling of bullets and { }, to get a nicer display *)
- let pred n = max 0 (n-1) in
- let ind, nl, new_beginend = match cmd with
- | VernacSubproof _ -> pred ind, nl, (pred ind)::beginend
- | VernacEndSubproof -> List.hd beginend, false, List.tl beginend
- | VernacBullet _ -> pred ind, nl, beginend
- | _ -> ind, nl, beginend
- in
- let pp =
- (if nl then fnl () else mt ()) ++
- (hov (ind+1) (str (String.make ind ' ') ++ Ppvernac.pr_vernac cmd))
- in
- (new_ngl, new_nl, new_beginend, pp :: ppl)
-
-let show_script ?proof () =
- try
- let prf =
- try match proof with
- | None -> Some (Pfedit.get_current_proof_name ())
- | Some (p,_) -> Some (p.Proof_global.id)
- with Proof_global.NoCurrentProof -> None
- in
- let cmds = get_script prf in
- let _,_,_,indented_cmds =
- List.fold_left indent_script_item ((1,[]),false,[],[]) cmds
- in
- let indented_cmds = List.rev (indented_cmds) in
- msg_notice (v 0 (prlist_with_sep fnl (fun x -> x) indented_cmds))
- with Vcs_aux.Expired -> ()
-
(* Export hooks *)
let state_computed_hook = Hooks.state_computed_hook
let state_ready_hook = Hooks.state_ready_hook
let parse_error_hook = Hooks.parse_error_hook
-let execution_error_hook = Hooks.execution_error_hook
let forward_feedback_hook = Hooks.forward_feedback_hook
let process_error_hook = Hooks.process_error_hook
-let interp_hook = Hooks.interp_hook
-let with_fail_hook = Hooks.with_fail_hook
let unreachable_state_hook = Hooks.unreachable_state_hook
-let get_fix_exn () = !State.fix_exn_ref
+let () = Hook.set Obligations.stm_get_fix_exn (fun () -> !State.fix_exn_ref)
let tactic_being_run_hook = Hooks.tactic_being_run_hook
(* vim:set foldmethod=marker: *)
diff --git a/stm/stm.mli b/stm/stm.mli
index b8a2a3859..0f0a3c4e1 100644
--- a/stm/stm.mli
+++ b/stm/stm.mli
@@ -184,7 +184,6 @@ val register_proof_block_delimiter :
val state_computed_hook : (Stateid.t -> in_cache:bool -> unit) Hook.t
val parse_error_hook :
(Feedback.edit_or_state_id -> Loc.t -> Pp.std_ppcmds -> unit) Hook.t
-val execution_error_hook : (Stateid.t -> Loc.t -> Pp.std_ppcmds -> unit) Hook.t
val unreachable_state_hook : (Stateid.t -> Exninfo.iexn -> unit) Hook.t
(* ready means that master has it at hand *)
val state_ready_hook : (Stateid.t -> unit) Hook.t
@@ -213,12 +212,6 @@ val interp : bool -> vernac_expr located -> unit
(* Queries for backward compatibility *)
val current_proof_depth : unit -> int
val get_all_proof_names : unit -> Id.t list
-val get_current_proof_name : unit -> Id.t option
-val show_script : ?proof:Proof_global.closed_proof -> unit -> unit
(* Hooks to be set by other Coq components in order to break file cycles *)
val process_error_hook : Future.fix_exn Hook.t
-val interp_hook : (?verbosely:bool -> ?proof:Proof_global.closed_proof ->
- Loc.t * Vernacexpr.vernac_expr -> unit) Hook.t
-val with_fail_hook : (bool -> (unit -> unit) -> unit) Hook.t
-val get_fix_exn : unit -> (Exninfo.iexn -> Exninfo.iexn)
diff --git a/stm/stm.mllib b/stm/stm.mllib
index 939ee187a..4b254e811 100644
--- a/stm/stm.mllib
+++ b/stm/stm.mllib
@@ -4,7 +4,6 @@ Vcs
TQueue
WorkerPool
Vernac_classifier
-Lemmas
CoqworkmgrApi
AsyncTaskQueue
Stm
diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml
index b7dd5f2a1..624b9ced7 100644
--- a/tools/coq_makefile.ml
+++ b/tools/coq_makefile.ml
@@ -51,7 +51,7 @@ let lib_dirs =
["kernel"; "lib"; "library"; "parsing";
"pretyping"; "interp"; "printing"; "intf";
"proofs"; "tactics"; "tools"; "ltacprof";
- "toplevel"; "stm"; "grammar"; "config";
+ "vernac"; "stm"; "toplevel"; "grammar"; "config";
"ltac"; "engine"]
diff --git a/tools/coqmktop.ml b/tools/coqmktop.ml
index eaf938e8c..645b3665e 100644
--- a/tools/coqmktop.ml
+++ b/tools/coqmktop.ml
@@ -75,6 +75,7 @@ let std_includes basedir =
let rebase d = match basedir with None -> d | Some base -> base / d in
["-I"; rebase ".";
"-I"; rebase "lib";
+ "-I"; rebase "vernac"; (* For Mltop *)
"-I"; rebase "toplevel";
"-I"; rebase "kernel/byterun";
"-I"; Envars.camlp4lib () ] @
diff --git a/toplevel/toplevel.mllib b/toplevel/toplevel.mllib
index d68922363..10bf48647 100644
--- a/toplevel/toplevel.mllib
+++ b/toplevel/toplevel.mllib
@@ -1,19 +1,3 @@
-Himsg
-ExplainErr
-Class
-Locality
-Metasyntax
-Auto_ind_decl
-Search
-Indschemes
-Obligations
-Command
-Classes
-Record
-Assumptions
-Vernacinterp
-Mltop
-Vernacentries
Vernac
Usage
Coqloop
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index c1a659c38..f914f83b9 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -343,7 +343,7 @@ let compile verbosely f =
let univs, proofs = Stm.finish_tasks lfdv univs disch proofs tasks in
Library.save_library_raw lfdv sum lib univs proofs
-let compile v f =
+let compile v f =
ignore(CoqworkmgrApi.get 1);
compile v f;
CoqworkmgrApi.giveback 1
diff --git a/toplevel/assumptions.ml b/vernac/assumptions.ml
index 8865cd646..8865cd646 100644
--- a/toplevel/assumptions.ml
+++ b/vernac/assumptions.ml
diff --git a/toplevel/assumptions.mli b/vernac/assumptions.mli
index 072675783..072675783 100644
--- a/toplevel/assumptions.mli
+++ b/vernac/assumptions.mli
diff --git a/toplevel/auto_ind_decl.ml b/vernac/auto_ind_decl.ml
index 594f2e944..594f2e944 100644
--- a/toplevel/auto_ind_decl.ml
+++ b/vernac/auto_ind_decl.ml
diff --git a/toplevel/auto_ind_decl.mli b/vernac/auto_ind_decl.mli
index 60232ba8f..60232ba8f 100644
--- a/toplevel/auto_ind_decl.mli
+++ b/vernac/auto_ind_decl.mli
diff --git a/toplevel/class.ml b/vernac/class.ml
index 0dc799014..0dc799014 100644
--- a/toplevel/class.ml
+++ b/vernac/class.ml
diff --git a/toplevel/class.mli b/vernac/class.mli
index 5f9ae28f6..5f9ae28f6 100644
--- a/toplevel/class.mli
+++ b/vernac/class.mli
diff --git a/toplevel/classes.ml b/vernac/classes.ml
index 6512f3def..6512f3def 100644
--- a/toplevel/classes.ml
+++ b/vernac/classes.ml
diff --git a/toplevel/classes.mli b/vernac/classes.mli
index d2cb788ea..d2cb788ea 100644
--- a/toplevel/classes.mli
+++ b/vernac/classes.mli
diff --git a/toplevel/command.ml b/vernac/command.ml
index 049f58aa2..049f58aa2 100644
--- a/toplevel/command.ml
+++ b/vernac/command.ml
diff --git a/toplevel/command.mli b/vernac/command.mli
index 616afb91f..616afb91f 100644
--- a/toplevel/command.mli
+++ b/vernac/command.mli
diff --git a/toplevel/discharge.ml b/vernac/discharge.ml
index e24d5e74f..e24d5e74f 100644
--- a/toplevel/discharge.ml
+++ b/vernac/discharge.ml
diff --git a/toplevel/discharge.mli b/vernac/discharge.mli
index 18d1b6776..18d1b6776 100644
--- a/toplevel/discharge.mli
+++ b/vernac/discharge.mli
diff --git a/toplevel/doc.tex b/vernac/doc.tex
index f2550fda1..f2550fda1 100644
--- a/toplevel/doc.tex
+++ b/vernac/doc.tex
diff --git a/toplevel/explainErr.ml b/vernac/explainErr.ml
index 17897460c..17897460c 100644
--- a/toplevel/explainErr.ml
+++ b/vernac/explainErr.ml
diff --git a/toplevel/explainErr.mli b/vernac/explainErr.mli
index a67c887af..a67c887af 100644
--- a/toplevel/explainErr.mli
+++ b/vernac/explainErr.mli
diff --git a/toplevel/himsg.ml b/vernac/himsg.ml
index 6cff805fc..6cff805fc 100644
--- a/toplevel/himsg.ml
+++ b/vernac/himsg.ml
diff --git a/toplevel/himsg.mli b/vernac/himsg.mli
index ced54fd27..ced54fd27 100644
--- a/toplevel/himsg.mli
+++ b/vernac/himsg.mli
diff --git a/toplevel/ind_tables.ml b/vernac/ind_tables.ml
index 85d0b6194..85d0b6194 100644
--- a/toplevel/ind_tables.ml
+++ b/vernac/ind_tables.ml
diff --git a/toplevel/ind_tables.mli b/vernac/ind_tables.mli
index 20f30d6d1..20f30d6d1 100644
--- a/toplevel/ind_tables.mli
+++ b/vernac/ind_tables.mli
diff --git a/toplevel/indschemes.ml b/vernac/indschemes.ml
index f7e3f0d95..f7e3f0d95 100644
--- a/toplevel/indschemes.ml
+++ b/vernac/indschemes.ml
diff --git a/toplevel/indschemes.mli b/vernac/indschemes.mli
index e5d79fd51..e5d79fd51 100644
--- a/toplevel/indschemes.mli
+++ b/vernac/indschemes.mli
diff --git a/stm/lemmas.ml b/vernac/lemmas.ml
index 55f33be39..55f33be39 100644
--- a/stm/lemmas.ml
+++ b/vernac/lemmas.ml
diff --git a/stm/lemmas.mli b/vernac/lemmas.mli
index 39c089be9..39c089be9 100644
--- a/stm/lemmas.mli
+++ b/vernac/lemmas.mli
diff --git a/toplevel/locality.ml b/vernac/locality.ml
index 03640676e..03640676e 100644
--- a/toplevel/locality.ml
+++ b/vernac/locality.ml
diff --git a/toplevel/locality.mli b/vernac/locality.mli
index 2ec392eef..2ec392eef 100644
--- a/toplevel/locality.mli
+++ b/vernac/locality.mli
diff --git a/toplevel/metasyntax.ml b/vernac/metasyntax.ml
index 0aaf6afd7..0aaf6afd7 100644
--- a/toplevel/metasyntax.ml
+++ b/vernac/metasyntax.ml
diff --git a/toplevel/metasyntax.mli b/vernac/metasyntax.mli
index 57c120402..57c120402 100644
--- a/toplevel/metasyntax.mli
+++ b/vernac/metasyntax.mli
diff --git a/toplevel/mltop.ml b/vernac/mltop.ml
index 2396cf04a..2396cf04a 100644
--- a/toplevel/mltop.ml
+++ b/vernac/mltop.ml
diff --git a/toplevel/mltop.mli b/vernac/mltop.mli
index 6633cb937..6633cb937 100644
--- a/toplevel/mltop.mli
+++ b/vernac/mltop.mli
diff --git a/toplevel/obligations.ml b/vernac/obligations.ml
index 9ada04317..6f3921903 100644
--- a/toplevel/obligations.ml
+++ b/vernac/obligations.ml
@@ -25,6 +25,8 @@ module NamedDecl = Context.Named.Declaration
let declare_fix_ref = ref (fun ?opaque _ _ _ _ _ _ -> assert false)
let declare_definition_ref = ref (fun _ _ _ _ _ -> assert false)
+let get_fix_exn, stm_get_fix_exn = Hook.make ()
+
let succfix (depth, fixrels) =
(succ depth, List.map succ fixrels)
@@ -485,7 +487,7 @@ let declare_definition prg =
let nf = Universes.nf_evars_and_universes_opt_subst (fun x -> None)
(Evd.evar_universe_context_subst prg.prg_ctx) in
let opaque = prg.prg_opaque in
- let fix_exn = Stm.get_fix_exn () in
+ let fix_exn = Hook.get get_fix_exn () in
let pl, ctx =
Evd.universe_context ?names:prg.prg_pl (Evd.from_ctx prg.prg_ctx) in
let ce =
@@ -566,7 +568,7 @@ let declare_mutual_definition l =
in
(* Declare the recursive definitions *)
let ctx = Evd.evar_context_universe_context first.prg_ctx in
- let fix_exn = Stm.get_fix_exn () in
+ let fix_exn = Hook.get get_fix_exn () in
let kns = List.map4 (!declare_fix_ref ~opaque (local, poly, kind) ctx)
fixnames fixdecls fixtypes fiximps in
(* Declare notations *)
diff --git a/toplevel/obligations.mli b/vernac/obligations.mli
index 80b689144..11366fe91 100644
--- a/toplevel/obligations.mli
+++ b/vernac/obligations.mli
@@ -24,6 +24,12 @@ val declare_definition_ref :
Safe_typing.private_constants Entries.definition_entry -> Impargs.manual_implicits
-> global_reference Lemmas.declaration_hook -> global_reference) ref
+(* This is a hack to make it possible for Obligations to craft a Qed
+ * behind the scenes. The fix_exn the Stm attaches to the Future proof
+ * is not available here, so we provide a side channel to get it *)
+val stm_get_fix_exn : (unit -> Exninfo.iexn -> Exninfo.iexn) Hook.t
+
+
val check_evars : env -> evar_map -> unit
val evar_dependencies : evar_map -> Evar.t -> Evar.Set.t
diff --git a/toplevel/record.ml b/vernac/record.ml
index d5faafaf8..d5faafaf8 100644
--- a/toplevel/record.ml
+++ b/vernac/record.ml
diff --git a/toplevel/record.mli b/vernac/record.mli
index c50e57786..c50e57786 100644
--- a/toplevel/record.mli
+++ b/vernac/record.mli
diff --git a/toplevel/search.ml b/vernac/search.ml
index e1b56b131..e1b56b131 100644
--- a/toplevel/search.ml
+++ b/vernac/search.ml
diff --git a/toplevel/search.mli b/vernac/search.mli
index c9167c485..c9167c485 100644
--- a/toplevel/search.mli
+++ b/vernac/search.mli
diff --git a/vernac/vernac.mllib b/vernac/vernac.mllib
new file mode 100644
index 000000000..94ef54f70
--- /dev/null
+++ b/vernac/vernac.mllib
@@ -0,0 +1,17 @@
+Lemmas
+Himsg
+ExplainErr
+Class
+Locality
+Metasyntax
+Auto_ind_decl
+Search
+Indschemes
+Obligations
+Command
+Classes
+Record
+Assumptions
+Vernacinterp
+Mltop
+Vernacentries
diff --git a/toplevel/vernacentries.ml b/vernac/vernacentries.ml
index 862a761b2..0bf81e7e5 100644
--- a/toplevel/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -515,11 +515,8 @@ let vernac_start_proof locality p kind l lettop =
let qed_display_script = ref true
let vernac_end_proof ?proof = function
- | Admitted -> save_proof ?proof Admitted
- | Proved (_,_) as e ->
- if is_verbose () && !qed_display_script && !Flags.coqtop_ui then
- Stm.show_script ?proof ();
- save_proof ?proof e
+ | Admitted -> save_proof ?proof Admitted
+ | Proved (_,_) as e -> save_proof ?proof e
(* A stupid macro that should be replaced by ``Exact c. Save.'' all along
the theories [??] *)
@@ -1868,6 +1865,7 @@ let vernac_bullet (bullet:Proof_global.Bullet.t) =
Proof_global.Bullet.put p bullet)
let vernac_show = let open Feedback in function
+ | ShowScript -> assert false (* Only the stm knows the script *)
| ShowGoal goalref ->
let info = match goalref with
| OpenSubgoals -> pr_open_subgoals ()
@@ -1882,7 +1880,6 @@ let vernac_show = let open Feedback in function
Constrextern.with_implicits msg_notice (pr_nth_open_subgoal n)
| ShowProof -> show_proof ()
| ShowNode -> show_node ()
- | ShowScript -> Stm.show_script ()
| ShowExistentials -> show_top_evars ()
| ShowUniverses -> show_universes ()
| ShowTree -> show_prooftree ()
@@ -1909,6 +1906,12 @@ let vernac_check_guard () =
exception End_of_input
+(* XXX: This won't properly set the proof mode, as of today, it is
+ controlled by the STM. Thus, we would need access information from
+ the classifier. The proper fix is to move it to the STM, however,
+ the way the proof mode is set there makes the task non trivial
+ without a considerable amount of refactoring.
+ *)
let vernac_load interp fname =
let interp x =
let proof_mode = Proof_global.get_default_proof_mode_name () in
@@ -1936,16 +1939,45 @@ let vernac_load interp fname =
let interp ?proof ~loc locality poly c =
prerr_endline (fun () -> "interpreting: " ^ Pp.string_of_ppcmds (Ppvernac.pr_vernac c));
match c with
- (* Done later in this file *)
+ (* The below vernac are candidates for removal from the main type
+ and to be put into a new doc_command datatype: *)
+
| VernacLoad _ -> assert false
+
+ (* Done later in this file *)
| VernacFail _ -> assert false
| VernacTime _ -> assert false
| VernacRedirect _ -> assert false
| VernacTimeout _ -> assert false
| VernacStm _ -> assert false
+ (* The STM should handle that, but LOAD bypasses the STM... *)
+ | VernacAbortAll -> CErrors.user_err (str "AbortAll cannot be used through the Load command")
+ | VernacRestart -> CErrors.user_err (str "Restart cannot be used through the Load command")
+ | VernacUndo _ -> CErrors.user_err (str "Undo cannot be used through the Load command")
+ | VernacUndoTo _ -> CErrors.user_err (str "UndoTo cannot be used through the Load command")
+ | VernacBacktrack _ -> CErrors.user_err (str "Backtrack cannot be used through the Load command")
+
+ (* Toplevel control *)
+ | VernacToplevelControl e -> raise e
+
+ (* Resetting *)
+ | VernacResetName _ -> anomaly (str "VernacResetName not handled by Stm")
+ | VernacResetInitial -> anomaly (str "VernacResetInitial not handled by Stm")
+ | VernacBack _ -> anomaly (str "VernacBack not handled by Stm")
+ | VernacBackTo _ -> anomaly (str "VernacBackTo not handled by Stm")
+
+ (* Horrible Hack that should die. *)
| VernacError e -> raise e
+ (* This one is possible to handle here *)
+ | VernacAbort id -> CErrors.user_err (str "Abort cannot be used through the Load command")
+
+ (* Handled elsewhere *)
+ | VernacProgram _
+ | VernacPolymorphic _
+ | VernacLocal _ -> assert false
+
(* Syntax *)
| VernacSyntaxExtension (local,sl) ->
vernac_syntax_extension locality local sl
@@ -2017,12 +2049,6 @@ let interp ?proof ~loc locality poly c =
| VernacWriteState s -> vernac_write_state s
| VernacRestoreState s -> vernac_restore_state s
- (* Resetting *)
- | VernacResetName _ -> anomaly (str "VernacResetName not handled by Stm")
- | VernacResetInitial -> anomaly (str "VernacResetInitial not handled by Stm")
- | VernacBack _ -> anomaly (str "VernacBack not handled by Stm")
- | VernacBackTo _ -> anomaly (str "VernacBackTo not handled by Stm")
-
(* Commands *)
| VernacCreateHintDb (dbname,b) -> vernac_create_hintdb locality dbname b
| VernacRemoveHints (dbnames,ids) -> vernac_remove_hints locality dbnames ids
@@ -2054,14 +2080,6 @@ let interp ?proof ~loc locality poly c =
| VernacRegister (id, r) -> vernac_register id r
| VernacComments l -> if_verbose Feedback.msg_info (str "Comments ok\n")
- (* The STM should handle that, but LOAD bypasses the STM... *)
- | VernacAbort id -> CErrors.user_err (str "Abort cannot be used through the Load command")
- | VernacAbortAll -> CErrors.user_err (str "AbortAll cannot be used through the Load command")
- | VernacRestart -> CErrors.user_err (str "Restart cannot be used through the Load command")
- | VernacUndo _ -> CErrors.user_err (str "Undo cannot be used through the Load command")
- | VernacUndoTo _ -> CErrors.user_err (str "UndoTo cannot be used through the Load command")
- | VernacBacktrack _ -> CErrors.user_err (str "Backtrack cannot be used through the Load command")
-
(* Proof management *)
| VernacGoal t -> vernac_start_proof locality poly Theorem [None,([],t,None)] false
| VernacFocus n -> vernac_focus n
@@ -2084,17 +2102,10 @@ let interp ?proof ~loc locality poly c =
Aux_file.record_in_aux_at loc "VernacProof" "tac:yes using:yes";
vernac_set_end_tac tac; vernac_set_used_variables l
| VernacProofMode mn -> Proof_global.set_proof_mode mn
- (* Toplevel control *)
- | VernacToplevelControl e -> raise e
(* Extensions *)
| VernacExtend (opn,args) -> Vernacinterp.call ?locality (opn,args)
- (* Handled elsewhere *)
- | VernacProgram _
- | VernacPolymorphic _
- | VernacLocal _ -> assert false
-
(* Vernaculars that take a locality flag *)
let check_vernac_supports_locality c l =
match l, c with
@@ -2253,6 +2264,3 @@ let interp ?(verbosely=true) ?proof (loc,c) =
in
if verbosely then Flags.verbosely (aux false) c
else aux false c
-
-let () = Hook.set Stm.interp_hook interp
-let () = Hook.set Stm.with_fail_hook with_fail
diff --git a/toplevel/vernacentries.mli b/vernac/vernacentries.mli
index 7cdc8dd06..7cdc8dd06 100644
--- a/toplevel/vernacentries.mli
+++ b/vernac/vernacentries.mli
diff --git a/toplevel/vernacinterp.ml b/vernac/vernacinterp.ml
index f26ef460d..f26ef460d 100644
--- a/toplevel/vernacinterp.ml
+++ b/vernac/vernacinterp.ml
diff --git a/toplevel/vernacinterp.mli b/vernac/vernacinterp.mli
index 5149b5416..5149b5416 100644
--- a/toplevel/vernacinterp.mli
+++ b/vernac/vernacinterp.mli
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-06 22:52:57 +0000