diff options
Diffstat (limited to 'plugins/ssrmatching')
| -rw-r--r-- | plugins/ssrmatching/ssrmatching.ml4 | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4 index 9dcc6c4cc..eb5f401e3 100644 --- a/plugins/ssrmatching/ssrmatching.ml4 +++ b/plugins/ssrmatching/ssrmatching.ml4 @@ -1353,6 +1353,7 @@ let fill_occ_term env cl occ sigma0 (sigma, t) = let pf_fill_occ_term gl occ t = let sigma0 = project gl and env = pf_env gl and concl = pf_concl gl in + let concl = EConstr.Unsafe.to_constr concl in let cl,(_,t) = fill_occ_term env concl occ sigma0 t in cl, t @@ -1388,6 +1389,7 @@ let ssrpatterntac _ist (arg_ist,arg) gl = let pat = interp_rpattern arg_ist gl arg in let sigma0 = project gl in let concl0 = pf_concl gl in + let concl0 = EConstr.Unsafe.to_constr concl0 in let (t, uc), concl_x = fill_occ_pattern (Global.env()) sigma0 concl0 pat noindex 1 in let t = EConstr.of_constr t in @@ -1416,6 +1418,7 @@ let ssrinstancesof ist arg gl = let ok rhs lhs ise = true in (* not (Term.eq_constr lhs (Evarutil.nf_evar ise rhs)) in *) let env, sigma, concl = pf_env gl, project gl, pf_concl gl in + let concl = EConstr.Unsafe.to_constr concl in let sigma0, cpat = interp_cpattern ist gl arg None in let pat = match cpat with T x -> x | _ -> errorstrm (str"Not supported") in let etpat, tpat = mk_tpattern env sigma (sigma0,pat) (ok pat) L2R pat in |