Merge PR #9129: [proof] Removal of imperative state ; interpretation layers only.

Ack-by: SkySkimmer
Reviewed-by: aspiwack
Ack-by: ejgallego
Ack-by: gares
Ack-by: herbelin
Reviewed-by: mattam82
Ack-by: maximedenes

1 files changed, 11 insertions, 10 deletions

diff --git a/ide/idetop.ml b/ide/idetop.ml
index 608577b297..f744ce2ee3 100644
--- a/ide/idetop.ml
+++ b/ide/idetop.ml
@@ -231,30 +231,30 @@ let goals () =
   let doc = get_doc () in
   set_doc @@ Stm.finish ~doc;
   try
-    let newp = Proof_global.give_me_the_proof () in
+    let newp = Vernacstate.Proof_global.give_me_the_proof () in
     if Proof_diffs.show_diffs () then begin
       let oldp = Stm.get_prev_proof ~doc (Stm.get_current_state ~doc) in
       let diff_goal_map = Proof_diffs.make_goal_map oldp newp in
       Some (export_pre_goals Proof.(data newp) (process_goal_diffs diff_goal_map oldp))
     end else
       Some (export_pre_goals Proof.(data newp) process_goal)
-  with Proof_global.NoCurrentProof -> None;;
+  with Vernacstate.Proof_global.NoCurrentProof -> None;;
 
 let evars () =
   try
     let doc = get_doc () in
     set_doc @@ Stm.finish ~doc;
-    let pfts = Proof_global.give_me_the_proof () in
+    let pfts = Vernacstate.Proof_global.give_me_the_proof () in
     let Proof.{ sigma } = Proof.data pfts in
     let exl = Evar.Map.bindings (Evd.undefined_map sigma) in
     let map_evar ev = { Interface.evar_info = string_of_ppcmds (pr_evar sigma ev); } in
     let el = List.map map_evar exl in
     Some el
-  with Proof_global.NoCurrentProof -> None
+  with Vernacstate.Proof_global.NoCurrentProof -> None
 
 let hints () =
   try
-    let pfts = Proof_global.give_me_the_proof () in
+    let pfts = Vernacstate.Proof_global.give_me_the_proof () in
     let Proof.{ goals; sigma } = Proof.data pfts in
     match goals with
     | [] -> None
@@ -263,7 +263,7 @@ let hints () =
       let get_hint_hyp env d accu = hyp_next_tac sigma env d :: accu in
       let hint_hyps = List.rev (Environ.fold_named_context get_hint_hyp env ~init: []) in
       Some (hint_hyps, concl_next_tac)
-  with Proof_global.NoCurrentProof -> None
+  with Vernacstate.Proof_global.NoCurrentProof -> None
 
 
 (** Other API calls *)
@@ -284,11 +284,11 @@ let status force =
     List.rev_map Names.Id.to_string l
   in
   let proof =
-    try Some (Names.Id.to_string (Proof_global.get_current_proof_name ()))
-    with Proof_global.NoCurrentProof -> None
+    try Some (Names.Id.to_string (Vernacstate.Proof_global.get_current_proof_name ()))
+    with Vernacstate.Proof_global.NoCurrentProof -> None
   in
   let allproofs =
-    let l = Proof_global.get_all_proof_names () in
+    let l = Vernacstate.Proof_global.get_all_proof_names () in
     List.map Names.Id.to_string l
   in
   {
@@ -336,7 +336,8 @@ let import_search_constraint = function
   | Interface.Include_Blacklist -> Search.Include_Blacklist
 
 let search flags =
-  List.map export_coq_object (Search.interface_search (
+  let pstate = Vernacstate.Proof_global.get () in
+  List.map export_coq_object (Search.interface_search ?pstate (
     List.map (fun (c, b) -> (import_search_constraint c, b)) flags)
   )