diff options
Diffstat (limited to 'plugins/ssrmatching')
| -rw-r--r-- | plugins/ssrmatching/ssrmatching.ml4 | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4 index 86cc928c8..cc39b7260 100644 --- a/plugins/ssrmatching/ssrmatching.ml4 +++ b/plugins/ssrmatching/ssrmatching.ml4 @@ -481,7 +481,9 @@ let evars_for_FO ~hack env sigma0 (ise0:evar_map) c0 = (* p_origin can be passed to obtain a better error message *) let mk_tpattern ?p_origin ?(hack=false) env sigma0 (ise, t) ok dir p = let k, f, a = - let f, a = Reductionops.whd_betaiota_stack ise p in + let f, a = Reductionops.whd_betaiota_stack ise (EConstr.of_constr p) in + let f = EConstr.Unsafe.to_constr f in + let a = List.map EConstr.Unsafe.to_constr a in match kind_of_term f with | Const (p,_) -> let np = proj_nparams p in |