aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins
diff options
context:
space:
mode:
authorGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2018-02-19 14:25:15 +0100
committerGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2018-03-06 09:59:50 +0100
commit601f41b23093e83b25c84d7e3701fa24ffe2dbca (patch)
treec8ea021cff0d67d1b161a468d7819ee959cb2d6b /plugins
parent15331729aaab16678c2f7e29dd391f72df53d76e (diff)
ssr: use `apply_type ~typecheck:true` everywhere (fix #6634)
Diffstat (limited to 'plugins')
-rw-r--r--plugins/ssr/ssrcommon.ml4
-rw-r--r--plugins/ssr/ssrcommon.mli2
-rw-r--r--plugins/ssr/ssrelim.ml2
-rw-r--r--plugins/ssr/ssrequality.ml2
-rw-r--r--plugins/ssr/ssrtacticals.ml2
5 files changed, 4 insertions, 8 deletions
diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml
index 5163ec7b3..511c83269 100644
--- a/plugins/ssr/ssrcommon.ml
+++ b/plugins/ssr/ssrcommon.ml
@@ -768,7 +768,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 ~typecheck:false (EConstr.of_constr (mkProd (Name id', t, cl')))
+ Proofview.V82.of_tactic (Tactics.apply_type ~typecheck:true (EConstr.of_constr (mkProd (Name id', t, cl')))
[EConstr.of_constr (mkVar id)]) gl
| NamedDecl.LocalDef (_, v, t), _ ->
Proofview.V82.of_tactic
@@ -1199,7 +1199,7 @@ let pf_interp_gen_aux 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 ~typecheck:false x xs)
+let apply_type x xs = Proofview.V82.of_tactic (Tactics.apply_type ~typecheck:true x xs)
let genclrtac cl cs clr =
let tclmyORELSE tac1 tac2 gl =
diff --git a/plugins/ssr/ssrcommon.mli b/plugins/ssr/ssrcommon.mli
index 7c16e1ba9..2b8f1d540 100644
--- a/plugins/ssr/ssrcommon.mli
+++ b/plugins/ssr/ssrcommon.mli
@@ -414,6 +414,8 @@ val clr_of_wgen :
val unfold : EConstr.t list -> unit Proofview.tactic
+val apply_type : EConstr.types -> EConstr.t list -> Proofview.V82.tac
+
(* New code ****************************************************************)
(* To call old code *)
diff --git a/plugins/ssr/ssrelim.ml b/plugins/ssr/ssrelim.ml
index 33ebe26b6..717657a24 100644
--- a/plugins/ssr/ssrelim.ml
+++ b/plugins/ssr/ssrelim.ml
@@ -30,8 +30,6 @@ module RelDecl = Context.Rel.Declaration
(** The "case" and "elim" tactic *)
-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
* checks if the eliminator is recursive or not *)
diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml
index 71cde0ca1..f45a191b7 100644
--- a/plugins/ssr/ssrequality.ml
+++ b/plugins/ssr/ssrequality.ml
@@ -384,8 +384,6 @@ 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 ~typecheck:false x xs)
-
let rwcltac cl rdx dir sr gl =
let n, r_n,_, ucst = pf_abs_evars gl sr in
let r_n' = pf_abs_cterm gl n r_n in
diff --git a/plugins/ssr/ssrtacticals.ml b/plugins/ssr/ssrtacticals.ml
index 21ad6e6ce..b29c83eff 100644
--- a/plugins/ssr/ssrtacticals.ml
+++ b/plugins/ssr/ssrtacticals.ml
@@ -127,8 +127,6 @@ let endclausestac id_map clseq gl_id cl0 gl =
if List.for_all not_hyp' all_ids && not c_hidden then mktac [] gl else
errorstrm Pp.(str "tampering with discharged assumptions of \"in\" tactical")
-let apply_type x xs = Proofview.V82.of_tactic (Tactics.apply_type ~typecheck:false x xs)
-
let tclCLAUSES tac (gens, clseq) gl =
if clseq = InGoal || clseq = InSeqGoal then tac gl else
let clr_gens = pf_clauseids gl gens clseq in