diff options
author | Maxime Dénès <mail@maximedenes.fr> | 2018-03-08 09:19:02 +0100 |
---|---|---|
committer | Maxime Dénès <mail@maximedenes.fr> | 2018-03-08 09:19:02 +0100 |
commit | dc9af4eb4be26f7656a6c5c8e8c80b44011c1734 (patch) | |
tree | 404c2fba550ce9b3779354d095bb416fa2869e44 /plugins/ssr/ssrcommon.ml | |
parent | 144517d764f11b8b79e8f7adfeca0d075dd4ac19 (diff) | |
parent | 601f41b23093e83b25c84d7e3701fa24ffe2dbca (diff) |
Merge PR #6783: ssr: use `apply_type ~typecheck:true` everywhere (fix #6634)
Diffstat (limited to 'plugins/ssr/ssrcommon.ml')
-rw-r--r-- | plugins/ssr/ssrcommon.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml index 007d139a3..43c29a08a 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 = |