[geninterp] Track polymorphic status in tactic interpretation.

18 files changed, 99 insertions, 55 deletions

diff --git a/plugins/ltac/extratactics.mlg b/plugins/ltac/extratactics.mlg
index 8bcf85b04a..f5098d2a34 100644
--- a/plugins/ltac/extratactics.mlg
+++ b/plugins/ltac/extratactics.mlg
@@ -53,6 +53,7 @@ let with_delayed_uconstr ist c tac =
     fail_evar = false;
     expand_evars = true;
     program_mode = false;
+    polymorphic = false;
  } in
   let c = Tacinterp.type_uconstr ~flags ist c in
   Tacticals.New.tclDELAYEDWITHHOLES false c tac
@@ -348,6 +349,7 @@ let constr_flags () = {
   Pretyping.fail_evar = false;
   Pretyping.expand_evars = true;
   Pretyping.program_mode = false;
+  Pretyping.polymorphic = false;
 }
 
 let refine_tac ist simple with_classes c =
diff --git a/plugins/ltac/g_auto.mlg b/plugins/ltac/g_auto.mlg
index 3a4b0571d4..523c7c8305 100644
--- a/plugins/ltac/g_auto.mlg
+++ b/plugins/ltac/g_auto.mlg
@@ -58,6 +58,7 @@ let eval_uconstrs ist cs =
     fail_evar = false;
     expand_evars = true;
     program_mode = false;
+    polymorphic = false;
   } in
   let map c env sigma = c env sigma in
   List.map (fun c -> map (Tacinterp.type_uconstr ~flags ist c)) cs
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 06d7d86dc6..75565c1a34 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -618,7 +618,9 @@ let solve_remaining_by env sigma holes by =
     in
     (* Only solve independent holes *)
     let indep = List.map_filter map holes in
-    let ist = { Geninterp.lfun = Id.Map.empty; extra = Geninterp.TacStore.empty } in
+    let ist = { Geninterp.lfun = Id.Map.empty
+              ; poly = false
+              ; extra = Geninterp.TacStore.empty } in
     let solve_tac = match tac with
     | Genarg.GenArg (Genarg.Glbwit tag, tac) ->
       Ftactic.run (Geninterp.interp tag ist tac) (fun _ -> Proofview.tclUNIT ())
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index e0fa46bd87..4398fb14ab 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -138,9 +138,10 @@ let f_debug : debug_info TacStore.field = TacStore.field ()
 let f_trace : ltac_trace TacStore.field = TacStore.field ()
 
 (* Signature for interpretation: val_interp and interpretation functions *)
-type interp_sign = Geninterp.interp_sign = {
-  lfun : value Id.Map.t;
-  extra : TacStore.t }
+type interp_sign = Geninterp.interp_sign =
+  { lfun : value Id.Map.t
+  ; poly : bool
+  ; extra : TacStore.t }
 
 let extract_trace ist =
   if is_traced () then match TacStore.get ist.extra f_trace with
@@ -544,7 +545,7 @@ let interp_gen kind ist pattern_mode flags env sigma c =
   let (_, dummy_proofview) = Proofview.init sigma [] in
 
   (* Again this is called at times with no open proof! *)
-  let name, poly = Id.of_string "tacinterp", false in
+  let name, poly = Id.of_string "tacinterp", ist.poly in
   let (trace,_,_,_) = Proofview.apply ~name ~poly env (push_trace (loc_of_glob_constr term,LtacConstrInterp (term,vars)) ist) dummy_proofview in
   let (evd,c) =
     catch_error trace (understand_ltac flags env sigma vars kind) term
@@ -561,11 +562,13 @@ let constr_flags () = {
   fail_evar = true;
   expand_evars = true;
   program_mode = false;
+  polymorphic = false;
 }
 
 (* Interprets a constr; expects evars to be solved *)
 let interp_constr_gen kind ist env sigma c =
-  interp_gen kind ist false (constr_flags ()) env sigma c
+  let flags = { (constr_flags ()) with polymorphic = ist.Geninterp.poly } in
+  interp_gen kind ist false flags env sigma c
 
 let interp_constr = interp_constr_gen WithoutTypeConstraint
 
@@ -577,6 +580,7 @@ let open_constr_use_classes_flags () = {
   fail_evar = false;
   expand_evars = true;
   program_mode = false;
+  polymorphic = false;
 }
 
 let open_constr_no_classes_flags () = {
@@ -585,6 +589,7 @@ let open_constr_no_classes_flags () = {
   fail_evar = false;
   expand_evars = true;
   program_mode = false;
+  polymorphic = false;
 }
 
 let pure_open_constr_flags = {
@@ -593,6 +598,7 @@ let pure_open_constr_flags = {
   fail_evar = false;
   expand_evars = false;
   program_mode = false;
+  polymorphic = false;
 }
 
 (* Interprets an open constr *)
@@ -1016,6 +1022,7 @@ let type_uconstr ?(flags = (constr_flags ()))
     ltac_idents = closure.idents;
     ltac_genargs = Id.Map.empty;
   } in
+  let flags = { flags with polymorphic = ist.Geninterp.poly } in
   understand_ltac flags env sigma vars expected_type term
   end
 
@@ -1141,6 +1148,7 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with
   (* For extensions *)
   | TacAlias {loc; v=(s,l)} ->
       let alias = Tacenv.interp_alias s in
+      Proofview.tclProofInfo [@ocaml.warning "-3"] >>= fun (_name, poly) ->
       let (>>=) = Ftactic.bind in
       let interp_vars = Ftactic.List.map (fun v -> interp_tacarg ist v) l in
       let tac l =
@@ -1148,8 +1156,9 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with
         let lfun = List.fold_right2 addvar alias.Tacenv.alias_args l ist.lfun in
         Ftactic.lift (push_trace (loc,LtacNotationCall s) ist) >>= fun trace ->
         let ist = {
-          lfun = lfun;
-          extra = TacStore.set ist.extra f_trace trace; } in
+          lfun
+        ; poly
+        ; extra = TacStore.set ist.extra f_trace trace } in
         val_interp ist alias.Tacenv.alias_body >>= fun v ->
         Ftactic.lift (tactic_of_value ist v)
       in
@@ -1202,12 +1211,13 @@ and interp_ltac_reference ?loc' mustbetac ist r : Val.t Ftactic.t =
       if mustbetac then Ftactic.return (coerce_to_tactic loc id v) else Ftactic.return v
       end
   | ArgArg (loc,r) ->
+      Proofview.tclProofInfo [@ocaml.warning "-3"] >>= fun (_name, poly) ->
       let ids = extract_ids [] ist.lfun Id.Set.empty in
       let loc_info = (Option.default loc loc',LtacNameCall r) in
       let extra = TacStore.set ist.extra f_avoid_ids ids in
       push_trace loc_info ist >>= fun trace ->
       let extra = TacStore.set extra f_trace trace in
-      let ist = { lfun = Id.Map.empty; extra = extra; } in
+      let ist = { lfun = Id.Map.empty; poly; extra } in
       let appl = GlbAppl[r,[]] in
       Profile_ltac.do_profile "interp_ltac_reference" trace ~count_call:false
         (val_interp ~appl ist (Tacenv.interp_ltac r))
@@ -1255,6 +1265,7 @@ and interp_tacarg ist arg : Val.t Ftactic.t =
 
 (* Interprets an application node *)
 and interp_app loc ist fv largs : Val.t Ftactic.t =
+  Proofview.tclProofInfo [@ocaml.warning "-3"] >>= fun (_name, poly) ->
   let (>>=) = Ftactic.bind in
   let fail = Tacticals.New.tclZEROMSG (str "Illegal tactic application.") in
   if has_type fv (topwit wit_tacvalue) then
@@ -1272,9 +1283,11 @@ and interp_app loc ist fv largs : Val.t Ftactic.t =
       if List.is_empty lvar then
         begin wrap_error
             begin
-              let ist = {
-                lfun = newlfun;
-                extra = TacStore.set ist.extra f_trace []; } in
+              let ist =
+                { lfun = newlfun
+                ; poly
+                ; extra = TacStore.set ist.extra f_trace []
+                } in
               Profile_ltac.do_profile "interp_app" trace ~count_call:false
                 (catch_error_tac trace (val_interp ist body)) >>= fun v ->
               Ftactic.return (name_vfun (push_appl appl largs) v)
@@ -1312,8 +1325,10 @@ and tactic_of_value ist vle =
   if has_type vle (topwit wit_tacvalue) then
   match to_tacvalue vle with
   | VFun (appl,trace,lfun,[],t) ->
+    Proofview.tclProofInfo [@ocaml.warning "-3"] >>= fun (_name, poly) ->
       let ist = {
         lfun = lfun;
+        poly;
         extra = TacStore.set ist.extra f_trace []; } in
       let tac = name_if_glob appl (eval_tactic ist t) in
       Profile_ltac.do_profile "tactic_of_value" trace (catch_error_tac trace tac)
@@ -1383,6 +1398,7 @@ and interp_letin ist llc u =
 (** [interp_match_success lz ist succ] interprets a single matching success
     (of type {!Tactic_matching.t}). *)
 and interp_match_success ist { Tactic_matching.subst ; context ; terms ; lhs } =
+  Proofview.tclProofInfo [@ocaml.warning "-3"] >>= fun (_name, poly) ->
   let (>>=) = Ftactic.bind in
   let lctxt = Id.Map.map interp_context context in
   let hyp_subst = Id.Map.map Value.of_constr terms in
@@ -1391,9 +1407,11 @@ and interp_match_success ist { Tactic_matching.subst ; context ; terms ; lhs } =
   val_interp ist lhs >>= fun v ->
   if has_type v (topwit wit_tacvalue) then match to_tacvalue v with
   | VFun (appl,trace,lfun,[],t) ->
-      let ist = {
-        lfun = lfun;
-        extra = TacStore.set ist.extra f_trace trace; } in
+      let ist =
+        { lfun = lfun
+        ; poly
+        ; extra = TacStore.set ist.extra f_trace trace
+        } in
       let tac = eval_tactic ist t in
       let dummy = VFun (appl,extract_trace ist, Id.Map.empty, [], TacId []) in
       catch_error_tac trace (tac <*> Ftactic.return (of_tacvalue dummy))
@@ -1867,7 +1885,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
 
 let default_ist () =
   let extra = TacStore.set TacStore.empty f_debug (get_debug ()) in
-  { lfun = Id.Map.empty; extra = extra }
+  { lfun = Id.Map.empty; poly = false; extra = extra }
 
 let eval_tactic t =
   Proofview.tclUNIT () >>= fun () -> (* delay for [default_ist] *)
@@ -1907,11 +1925,12 @@ end
 
 
 let interp_tac_gen lfun avoid_ids debug t =
+  Proofview.tclProofInfo [@ocaml.warning "-3"] >>= fun (_name, poly) ->
   Proofview.Goal.enter begin fun gl ->
   let env = Proofview.Goal.env gl in
   let extra = TacStore.set TacStore.empty f_debug debug in
   let extra = TacStore.set extra f_avoid_ids avoid_ids in
-  let ist = { lfun = lfun; extra = extra } in
+  let ist = { lfun; poly; extra } in
   let ltacvars = Id.Map.domain lfun in
   interp_tactic ist
     (intern_pure_tactic { (Genintern.empty_glob_sign env) with ltacvars } t)
@@ -2052,13 +2071,15 @@ let interp_redexp env sigma r =
 (* Backwarding recursive needs of tactic glob/interp/eval functions *)
 
 let _ =
-  let eval lfun env sigma ty tac =
+  let eval lfun poly env sigma ty tac =
     let extra = TacStore.set TacStore.empty f_debug (get_debug ()) in
-    let ist = { lfun = lfun; extra; } in
+    let ist = { lfun; poly; extra; } in
     let tac = interp_tactic ist tac in
-    (* XXX: This depends on the global state which is bad; the hooking
-       mechanism should be modified. *)
-    let name, poly = Id.of_string "ltac_gen", false in
+    (* EJGA: We sould also pass the proof name if desired, for now
+       poly seems like enough to get reasonable behavior in practice
+     *)
+    let name, poly = Id.of_string "ltac_gen", poly in
+    let name, poly = Id.of_string "ltac_gen", poly in
     let (c, sigma) = Pfedit.refine_by_tactic ~name ~poly env sigma ty tac in
     (EConstr.of_constr c, sigma)
   in
diff --git a/plugins/ltac/tacinterp.mli b/plugins/ltac/tacinterp.mli
index d9c80bb835..22a092fa8b 100644
--- a/plugins/ltac/tacinterp.mli
+++ b/plugins/ltac/tacinterp.mli
@@ -39,9 +39,10 @@ module TacStore : Store.S with
   and type 'a field = 'a Geninterp.TacStore.field
 
 (** Signature for interpretation: val\_interp and interpretation functions *)
-type interp_sign = Geninterp.interp_sign = {
-  lfun : value Id.Map.t;
-  extra : TacStore.t }
+type interp_sign = Geninterp.interp_sign =
+  { lfun : value Id.Map.t
+  ; poly : bool
+  ; extra : TacStore.t }
 
 open Genintern
 
diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml
index 0ca7e904da..2a84469af0 100644
--- a/plugins/ssr/ssrcommon.ml
+++ b/plugins/ssr/ssrcommon.ml
@@ -246,6 +246,7 @@ let interp_refine ist gl rc =
     fail_evar = false;
     expand_evars = true;
     program_mode = false;
+    polymorphic = false;
   }
   in
   let sigma, c = Pretyping.understand_ltac flags (pf_env gl) (project gl) vars kind rc in
@@ -1175,7 +1176,7 @@ let genstac (gens, clr) =
   tclTHENLIST (old_cleartac clr :: List.rev_map gentac gens)
 
 let gen_tmp_ids
-  ?(ist=Geninterp.({ lfun = Id.Map.empty; extra = Tacinterp.TacStore.empty })) gl
+  ?(ist=Geninterp.({ lfun = Id.Map.empty; poly = false; extra = Tacinterp.TacStore.empty })) gl
 =
   let gl, ctx = pull_ctx gl in
   push_ctxs ctx
diff --git a/plugins/ssrmatching/ssrmatching.ml b/plugins/ssrmatching/ssrmatching.ml
index 4b5fa7bf27..1deb935d5c 100644
--- a/plugins/ssrmatching/ssrmatching.ml
+++ b/plugins/ssrmatching/ssrmatching.ml
@@ -1267,7 +1267,7 @@ let pf_fill_occ_term gl occ t =
   cl, t
 
 let cpattern_of_id id =
-  ' ', (DAst.make @@ GRef (VarRef  id, None), None), Some Geninterp.({ lfun = Id.Map.empty; extra = Tacinterp.TacStore.empty })
+  ' ', (DAst.make @@ GRef (VarRef  id, None), None), Some Geninterp.({ lfun = Id.Map.empty; poly = false; extra = Tacinterp.TacStore.empty })
 
 let is_wildcard ((_, (l, r), _) : cpattern) : bool = match DAst.get l, r with
   | _, Some { CAst.v = CHole _ } | GHole _, None -> true
diff --git a/pretyping/geninterp.ml b/pretyping/geninterp.ml
index 1f8b926365..32152ad0e4 100644
--- a/pretyping/geninterp.ml
+++ b/pretyping/geninterp.ml
@@ -82,9 +82,10 @@ let register_val0 wit tag =
 
 (** Interpretation functions *)
 
-type interp_sign = {
-  lfun : Val.t Id.Map.t;
-  extra : TacStore.t }
+type interp_sign =
+  { lfun : Val.t Id.Map.t
+  ; poly : bool
+  ; extra : TacStore.t }
 
 type ('glb, 'top) interp_fun = interp_sign -> 'glb -> 'top Ftactic.t
 
diff --git a/pretyping/geninterp.mli b/pretyping/geninterp.mli
index 606a6ebead..49d874289d 100644
--- a/pretyping/geninterp.mli
+++ b/pretyping/geninterp.mli
@@ -62,9 +62,10 @@ val register_val0 : ('raw, 'glb, 'top) genarg_type -> 'top Val.tag option -> uni
 
 module TacStore : Store.S
 
-type interp_sign = {
-  lfun : Val.t Id.Map.t;
-  extra : TacStore.t }
+type interp_sign =
+  { lfun : Val.t Id.Map.t
+  ; poly : bool
+  ; extra : TacStore.t }
 
 type ('glb, 'top) interp_fun = interp_sign -> 'glb -> 'top Ftactic.t
 
diff --git a/pretyping/globEnv.ml b/pretyping/globEnv.ml
index cd82b1993b..e76eb2a7de 100644
--- a/pretyping/globEnv.ml
+++ b/pretyping/globEnv.ml
@@ -183,7 +183,7 @@ let interp_ltac_id env id = ltac_interp_id env.lvar id
 module ConstrInterpObj =
 struct
   type ('r, 'g, 't) obj =
-    unbound_ltac_var_map -> env -> Evd.evar_map -> types -> 'g -> constr * Evd.evar_map
+    unbound_ltac_var_map -> bool -> env -> Evd.evar_map -> types -> 'g -> constr * Evd.evar_map
   let name = "constr_interp"
   let default _ = None
 end
@@ -192,8 +192,8 @@ module ConstrInterp = Genarg.Register(ConstrInterpObj)
 
 let register_constr_interp0 = ConstrInterp.register0
 
-let interp_glob_genarg env sigma ty arg =
+let interp_glob_genarg env poly sigma ty arg =
   let open Genarg in
   let GenArg (Glbwit tag, arg) = arg in
   let interp = ConstrInterp.obj tag in
-  interp env.lvar.ltac_genargs env.renamed_env sigma ty arg
+  interp env.lvar.ltac_genargs poly env.renamed_env sigma ty arg
diff --git a/pretyping/globEnv.mli b/pretyping/globEnv.mli
index 65ae495135..cdd36bbba6 100644
--- a/pretyping/globEnv.mli
+++ b/pretyping/globEnv.mli
@@ -19,7 +19,7 @@ open Evarutil
 
 val register_constr_interp0 :
   ('r, 'g, 't) Genarg.genarg_type ->
-    (unbound_ltac_var_map -> env -> evar_map -> types -> 'g -> constr * evar_map) -> unit
+    (unbound_ltac_var_map -> bool -> env -> evar_map -> types -> 'g -> constr * evar_map) -> unit
 
 (** {6 Pretyping name management} *)
 
@@ -85,5 +85,5 @@ val interp_ltac_id : t -> Id.t -> Id.t
 (** Interpreting a generic argument, typically a "ltac:(...)", taking
     into account the possible renaming *)
 
-val interp_glob_genarg : t -> evar_map -> constr ->
+val interp_glob_genarg : t -> bool -> evar_map -> constr ->
   Genarg.glob_generic_argument -> constr * evar_map
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 8e9a2e114b..23936d50b1 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -198,6 +198,7 @@ type inference_flags = {
   fail_evar : bool;
   expand_evars : bool;
   program_mode : bool;
+  polymorphic : bool;
 }
 
 (* Compute the set of still-undefined initial evars up to restriction
@@ -474,10 +475,10 @@ let mark_obligation_evar sigma k evc =
 (* in environment [env], with existential variables [sigma] and *)
 (* the type constraint tycon *)
 
-let rec pretype ~program_mode k0 resolve_tc (tycon : type_constraint) (env : GlobEnv.t) (sigma : evar_map) t =
+let rec pretype ~program_mode ~poly k0 resolve_tc (tycon : type_constraint) (env : GlobEnv.t) (sigma : evar_map) t =
   let inh_conv_coerce_to_tycon ?loc = inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc in
-  let pretype_type = pretype_type ~program_mode k0 resolve_tc in
-  let pretype = pretype ~program_mode k0 resolve_tc in
+  let pretype_type = pretype_type ~program_mode ~poly k0 resolve_tc in
+  let pretype = pretype ~program_mode ~poly k0 resolve_tc in
   let open Context.Rel.Declaration in
   let loc = t.CAst.loc in
   match DAst.get t with
@@ -497,7 +498,7 @@ let rec pretype ~program_mode k0 resolve_tc (tycon : type_constraint) (env : Glo
         try Evd.evar_key id sigma
         with Not_found -> error_evar_not_found ?loc !!env sigma id in
       let hyps = evar_filtered_context (Evd.find sigma evk) in
-      let sigma, args = pretype_instance ~program_mode k0 resolve_tc env sigma loc hyps evk inst in
+      let sigma, args = pretype_instance ~program_mode ~poly k0 resolve_tc env sigma loc hyps evk inst in
       let c = mkEvar (evk, args) in
       let j = Retyping.get_judgment_of !!env sigma c in
       inh_conv_coerce_to_tycon ?loc env sigma j tycon
@@ -530,7 +531,7 @@ let rec pretype ~program_mode k0 resolve_tc (tycon : type_constraint) (env : Glo
         match tycon with
         | Some ty -> sigma, ty
         | None -> new_type_evar env sigma loc in
-      let c, sigma = GlobEnv.interp_glob_genarg env sigma ty arg in
+      let c, sigma = GlobEnv.interp_glob_genarg env poly sigma ty arg in
       sigma, { uj_val = c; uj_type = ty }
 
   | GRec (fixkind,names,bl,lar,vdef) ->
@@ -983,7 +984,7 @@ let rec pretype ~program_mode k0 resolve_tc (tycon : type_constraint) (env : Glo
         in
         inh_conv_coerce_to_tycon ?loc env sigma resj tycon
 
-and pretype_instance ~program_mode k0 resolve_tc env sigma loc hyps evk update =
+and pretype_instance ~program_mode ~poly k0 resolve_tc env sigma loc hyps evk update =
   let f decl (subst,update,sigma) =
     let id = NamedDecl.get_id decl in
     let b = Option.map (replace_vars subst) (NamedDecl.get_value decl) in
@@ -1015,7 +1016,7 @@ and pretype_instance ~program_mode k0 resolve_tc env sigma loc hyps evk update =
     let sigma, c, update =
       try
         let c = List.assoc id update in
-        let sigma, c = pretype ~program_mode k0 resolve_tc (mk_tycon t) env sigma c in
+        let sigma, c = pretype ~program_mode ~poly k0 resolve_tc (mk_tycon t) env sigma c in
         check_body sigma id (Some c.uj_val);
         sigma, c.uj_val, List.remove_assoc id update
       with Not_found ->
@@ -1040,7 +1041,7 @@ and pretype_instance ~program_mode k0 resolve_tc env sigma loc hyps evk update =
   sigma, Array.map_of_list snd subst
 
 (* [pretype_type valcon env sigma c] coerces [c] into a type *)
-and pretype_type ~program_mode k0 resolve_tc valcon (env : GlobEnv.t) sigma c = match DAst.get c with
+and pretype_type ~program_mode ~poly k0 resolve_tc valcon (env : GlobEnv.t) sigma c = match DAst.get c with
   | GHole (knd, naming, None) ->
       let loc = loc_of_glob_constr c in
       (match valcon with
@@ -1067,7 +1068,7 @@ and pretype_type ~program_mode k0 resolve_tc valcon (env : GlobEnv.t) sigma c =
          let sigma = if program_mode then mark_obligation_evar sigma knd utj_val else sigma in
          sigma, { utj_val; utj_type = s})
   | _ ->
-      let sigma, j = pretype ~program_mode k0 resolve_tc empty_tycon env sigma c in
+      let sigma, j = pretype ~program_mode ~poly k0 resolve_tc empty_tycon env sigma c in
       let loc = loc_of_glob_constr c in
       let sigma, tj = Coercion.inh_coerce_to_sort ?loc !!env sigma j in
 	match valcon with
@@ -1082,6 +1083,7 @@ and pretype_type ~program_mode k0 resolve_tc valcon (env : GlobEnv.t) sigma c =
 
 let ise_pretype_gen flags env sigma lvar kind c =
   let program_mode = flags.program_mode in
+  let poly = flags.polymorphic in
   let hypnaming =
     if program_mode then ProgramNaming else KeepUserNameAndRenameExistingButSectionNames
   in
@@ -1089,13 +1091,13 @@ let ise_pretype_gen flags env sigma lvar kind c =
   let k0 = Context.Rel.length (rel_context !!env) in
   let sigma', c', c'_ty = match kind with
     | WithoutTypeConstraint ->
-      let sigma, j = pretype ~program_mode k0 flags.use_typeclasses empty_tycon env sigma c in
+      let sigma, j = pretype ~program_mode ~poly k0 flags.use_typeclasses empty_tycon env sigma c in
       sigma, j.uj_val, j.uj_type
     | OfType exptyp ->
-      let sigma, j = pretype ~program_mode k0 flags.use_typeclasses (mk_tycon exptyp) env sigma c in
+      let sigma, j = pretype ~program_mode ~poly k0 flags.use_typeclasses (mk_tycon exptyp) env sigma c in
       sigma, j.uj_val, j.uj_type
     | IsType ->
-      let sigma, tj = pretype_type ~program_mode k0 flags.use_typeclasses empty_valcon env sigma c in
+      let sigma, tj = pretype_type ~program_mode ~poly k0 flags.use_typeclasses empty_valcon env sigma c in
       sigma, tj.utj_val, mkSort tj.utj_type
   in
   process_inference_flags flags !!env sigma (sigma',c',c'_ty)
@@ -1106,6 +1108,7 @@ let default_inference_flags fail = {
   fail_evar = fail;
   expand_evars = true;
   program_mode = false;
+  polymorphic = false;
 }
 
 let no_classes_no_fail_inference_flags = {
@@ -1114,6 +1117,7 @@ let no_classes_no_fail_inference_flags = {
   fail_evar = false;
   expand_evars = true;
   program_mode = false;
+  polymorphic = false;
 }
 
 let all_and_fail_flags = default_inference_flags true
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index 3c875e69d2..1037cf6cc5 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -38,6 +38,7 @@ type inference_flags = {
   fail_evar : bool;
   expand_evars : bool;
   program_mode : bool;
+  polymorphic : bool;
 }
 
 val default_inference_flags : bool -> inference_flags
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 ())
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 *)