[geninterp] Track polymorphic status in tactic interpretation.

3 files changed, 12 insertions, 4 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/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 *)