diff options
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/ssr/ssrcommon.ml | 4 | ||||
| -rw-r--r-- | plugins/ssr/ssrelim.ml | 2 | ||||
| -rw-r--r-- | plugins/ssr/ssrequality.ml | 2 | ||||
| -rw-r--r-- | plugins/ssr/ssripats.ml | 2 | ||||
| -rw-r--r-- | plugins/ssr/ssrtacticals.ml | 2 |
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 |