From c0cff3a7ebb79d1142090108c56e9aa64c3b481d Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Wed, 13 Feb 2019 05:37:09 +0100
Subject: [geninterp] Track polymorphic status in tactic interpretation.

---
 proofs/evar_refiner.ml | 1 +
 proofs/proof_global.ml | 2 +-
 2 files changed, 2 insertions(+), 1 deletion(-)

(limited to 'proofs')

diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml
index 0f97a942ed..1a34105ab6 100644
--- a/proofs/evar_refiner.ml
+++ b/proofs/evar_refiner.ml
@@ -55,6 +55,7 @@ let w_refine (evk,evi) (ltac_var,rawc) sigma =
       Pretyping.fail_evar = false;
       Pretyping.expand_evars = true;
       Pretyping.program_mode = false;
+      Pretyping.polymorphic = false;
     } in
     try Pretyping.understand_ltac flags
       env sigma ltac_var (Pretyping.OfType evi.evar_concl) rawc
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 0fefb215e2..86d3d9601e 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -85,7 +85,7 @@ let with_current_proof f (ps, psl) =
     | None -> Proofview.tclUNIT ()
     | Some tac ->
       let open Geninterp in
-      let ist = { lfun = Id.Map.empty; extra = TacStore.empty } in
+      let ist = { lfun = Id.Map.empty; poly = pi2 ps.strength; extra = TacStore.empty } in
       let Genarg.GenArg (Genarg.Glbwit tag, tac) = tac in
       let tac = Geninterp.interp tag ist tac in
       Ftactic.run tac (fun _ -> Proofview.tclUNIT ())
-- 
cgit v1.2.3