apply_type: add option "typecheck" passed down to refine

5 files changed, 6 insertions, 6 deletions

diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml
index 7cdf05117..d25ecee06 100644
--- a/plugins/ssr/ssrcommon.ml
+++ b/plugins/ssr/ssrcommon.ml
@@ -745,7 +745,7 @@ let discharge_hyp (id', (id, mode)) gl =
   let cl' = Vars.subst_var id (pf_concl gl) in
   match pf_get_hyp gl id, mode with
   | NamedDecl.LocalAssum (_, t), _ | NamedDecl.LocalDef (_, _, t), "(" ->
-     Proofview.V82.of_tactic (Tactics.apply_type (EConstr.of_constr (mkProd (Name id', t, cl')))
+     Proofview.V82.of_tactic (Tactics.apply_type ~typecheck:false (EConstr.of_constr (mkProd (Name id', t, cl')))
        [EConstr.of_constr (mkVar id)]) gl
   | NamedDecl.LocalDef (_, v, t), _ ->
      Proofview.V82.of_tactic
@@ -1179,7 +1179,7 @@ let pf_interp_gen_aux ist gl to_ind ((oclr, occ), t) =
     false, pat, EConstr.mkProd (constr_name (project gl) c, pty, Tacmach.pf_concl gl), p, clr,ucst,gl
   else CErrors.user_err ?loc:(loc_of_cpattern t) (str "generalized term didn't match")
 
-let apply_type x xs = Proofview.V82.of_tactic (Tactics.apply_type x xs)
+let apply_type x xs = Proofview.V82.of_tactic (Tactics.apply_type ~typecheck:false x xs)
 
 let genclrtac cl cs clr =
   let tclmyORELSE tac1 tac2 gl =
diff --git a/plugins/ssr/ssrelim.ml b/plugins/ssr/ssrelim.ml
index 4e0b44a44..5782a7621 100644
--- a/plugins/ssr/ssrelim.ml
+++ b/plugins/ssr/ssrelim.ml
@@ -28,7 +28,7 @@ module RelDecl = Context.Rel.Declaration
 
 (** The "case" and "elim" tactic *)
 
-let apply_type x xs = Proofview.V82.of_tactic (Tactics.apply_type x xs)
+let apply_type x xs = Proofview.V82.of_tactic (Tactics.apply_type ~typecheck:false x xs)
 
 (* TASSI: given the type of an elimination principle, it finds the higher order
  * argument (index), it computes it's arity and the arity of the eliminator and
diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml
index 6032ed2af..11ebe4337 100644
--- a/plugins/ssr/ssrequality.ml
+++ b/plugins/ssr/ssrequality.ml
@@ -382,7 +382,7 @@ let is_construct_ref sigma c r =
   EConstr.isConstruct sigma c && eq_gr (ConstructRef (fst(EConstr.destConstruct sigma c))) r
 let is_ind_ref sigma c r = EConstr.isInd sigma c && eq_gr (IndRef (fst(EConstr.destInd sigma c))) r
 
-let apply_type x xs = Proofview.V82.of_tactic (Tactics.apply_type x xs)
+let apply_type x xs = Proofview.V82.of_tactic (Tactics.apply_type ~typecheck:false x xs)
 
 let rwcltac cl rdx dir sr gl =
   let n, r_n,_, ucst = pf_abs_evars gl sr in
diff --git a/plugins/ssr/ssripats.ml b/plugins/ssr/ssripats.ml
index 6c325cce4..b3be31b7b 100644
--- a/plugins/ssr/ssripats.ml
+++ b/plugins/ssr/ssripats.ml
@@ -41,7 +41,7 @@ module RelDecl = Context.Rel.Declaration
 (* They require guessing the view hints and the number of      *)
 (* implicits, respectively, which we do by brute force.        *)
 
-let apply_type x xs = Proofview.V82.of_tactic (apply_type x xs)
+let apply_type x xs = Proofview.V82.of_tactic (apply_type ~typecheck:false x xs)
 
 let new_tac = Proofview.V82.of_tactic
 
diff --git a/plugins/ssr/ssrtacticals.ml b/plugins/ssr/ssrtacticals.ml
index 5e43c8374..6514b186e 100644
--- a/plugins/ssr/ssrtacticals.ml
+++ b/plugins/ssr/ssrtacticals.ml
@@ -122,7 +122,7 @@ let endclausestac id_map clseq gl_id cl0 gl =
   if List.for_all not_hyp' all_ids && not c_hidden then mktac [] gl else
   CErrors.user_err (Pp.str "tampering with discharged assumptions of \"in\" tactical")
 
-let apply_type x xs = Proofview.V82.of_tactic (Tactics.apply_type x xs)
+let apply_type x xs = Proofview.V82.of_tactic (Tactics.apply_type ~typecheck:false x xs)
 
 let tclCLAUSES ist tac (gens, clseq) gl =
   if clseq = InGoal || clseq = InSeqGoal then tac gl else