aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2018-02-19 10:10:09 +0100
committerGravatar Maxime Dénès <mail@maximedenes.fr>2018-02-19 10:10:09 +0100
commitb2bc3eb2a2de6d0834bd6066d2b78c7ba0ed23f3 (patch)
treec6eb19e39559df2f55df8edf06d56e29223100ab /plugins
parent1cf756712b5a5216e3a0039fb9d831c8d8ba9cbf (diff)
parent9a4340d2fdba8452d04a47402b5c1ad7bcc7f97b (diff)
Merge PR #6648: [tactics] make apply_type safe
Diffstat (limited to 'plugins')
-rw-r--r--plugins/ssr/ssrcommon.ml4
-rw-r--r--plugins/ssr/ssrelim.ml2
-rw-r--r--plugins/ssr/ssrequality.ml2
-rw-r--r--plugins/ssr/ssripats.ml2
-rw-r--r--plugins/ssr/ssrtacticals.ml2
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