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

6 files changed, 21 insertions, 12 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index 2619620eb8..4e0ec1f7e4 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -143,7 +143,8 @@ let conclPattern concl pat tac =
   Proofview.Goal.enter begin fun gl ->
      let env = Proofview.Goal.env gl in
      let sigma = Tacmach.New.project gl in
-       constr_bindings env sigma >>= fun constr_bindings ->
+     constr_bindings env sigma >>= fun constr_bindings ->
+     Proofview.tclProofInfo [@ocaml.warning "-3"] >>= fun (_name, poly) ->
      let open Genarg in
      let open Geninterp in
      let inj c = match val_tag (topwit Stdarg.wit_constr) with
@@ -152,7 +153,9 @@ let conclPattern concl pat tac =
      in
      let fold id c accu = Id.Map.add id (inj c) accu in
      let lfun = Id.Map.fold fold constr_bindings Id.Map.empty in
-     let ist = { lfun; extra = TacStore.empty } in
+     let ist = { lfun
+               ; poly
+               ; extra = TacStore.empty } in
      match tac with
      | GenArg (Glbwit wit, tac) ->
       Ftactic.run (Geninterp.interp wit ist tac) (fun _ -> Proofview.tclUNIT ())
diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml
index d9c0a26f91..51708670f5 100644
--- a/tactics/autorewrite.ml
+++ b/tactics/autorewrite.ml
@@ -99,11 +99,15 @@ let one_base general_rewrite_maybe_in tac_main bas =
     Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma)
     (general_rewrite_maybe_in dir c' tc)
   end in
-  let lrul = List.map (fun h -> 
+  let open Proofview.Notations in
+  Proofview.tclProofInfo [@ocaml.warning "-3"] >>= fun (_name, poly) ->
+  let lrul = List.map (fun h ->
   let tac = match h.rew_tac with
   | None -> Proofview.tclUNIT ()
   | Some (Genarg.GenArg (Genarg.Glbwit wit, tac)) ->
-    let ist = { Geninterp.lfun = Id.Map.empty; extra = Geninterp.TacStore.empty } in
+    let ist = { Geninterp.lfun = Id.Map.empty
+              ; poly
+              ; extra = Geninterp.TacStore.empty } in
     Ftactic.run (Geninterp.interp wit ist tac) (fun _ -> Proofview.tclUNIT ())
   in
     (h.rew_ctx,h.rew_lemma,h.rew_l2r,tac)) lrul in
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index a3620f4081..44102afd74 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -933,11 +933,12 @@ module Search = struct
        try
          (* Instance may try to call this before a proof is set up!
             Thus, give_me_the_proof will fail. Beware! *)
-         let name, poly = try
-             let Proof.{ name; poly } = Proof.data Proof_global.(give_me_the_proof ()) in
-             name, poly
-           with | Proof_global.NoCurrentProof ->
-             Id.of_string "instance", false
+         let name, poly =
+           (* try
+            *   let Proof.{ name; poly } = Proof.data Proof_global.(give_me_the_proof ()) in
+            *   name, poly
+            * with | Proof_global.NoCurrentProof -> *)
+           Id.of_string "instance", false
          in
          let (), pv', (unsafe, shelved, gaveup), _ =
            Proofview.apply ~name ~poly env tac pv
diff --git a/tactics/hints.ml b/tactics/hints.ml
index 85d75f1010..3a7e67cb3f 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -1514,9 +1514,9 @@ let pr_hint_term env sigma cl =
     (str "No hint applicable for current goal")
 
 (* print all hints that apply to the concl of the current goal *)
-let pr_applicable_hint () =
+let pr_applicable_hint pf =
   let env = Global.env () in
-  let pts = Proof_global.give_me_the_proof () in
+  let pts = Proof_global.give_me_the_proof pf in
   let Proof.{goals;sigma} = Proof.data pts in
   match goals with
   | [] -> CErrors.user_err Pp.(str "No focused goal.")
diff --git a/tactics/hints.mli b/tactics/hints.mli
index dd2c63d351..e84e423faa 100644
--- a/tactics/hints.mli
+++ b/tactics/hints.mli
@@ -294,7 +294,7 @@ val wrap_hint_warning_fun : env -> evar_map ->
 (** Printing  hints *)
 
 val pr_searchtable : env -> evar_map -> Pp.t
-val pr_applicable_hint : unit -> Pp.t
+val pr_applicable_hint : Proof_global.t -> Pp.t
 val pr_hint_ref : env -> evar_map -> GlobRef.t -> Pp.t
 val pr_hint_db_by_name : env -> evar_map -> hint_db_name -> Pp.t
 val pr_hint_db_env : env -> evar_map -> Hint_db.t -> Pp.t
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index b8308dc49b..206f35c8ba 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1161,6 +1161,7 @@ let tactic_infer_flags with_evar = {
   Pretyping.fail_evar = not with_evar;
   Pretyping.expand_evars = true;
   Pretyping.program_mode = false;
+  Pretyping.polymorphic = false;
 }
 
 type evars_flag = bool     (* true = pose evars       false = fail on evars *)