diff options
Diffstat (limited to 'pretyping/tacred.ml')
| -rw-r--r-- | pretyping/tacred.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index 290d77b1b..a3983737d 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -1164,7 +1164,7 @@ let pattern_occs loccs_trm = { e_redfun = begin fun env sigma c -> let sigma = Sigma.to_evar_map sigma in let abstr_trm, sigma = List.fold_right (abstract_scheme env) loccs_trm (EConstr.Unsafe.to_constr c,sigma) in try - let _ = Typing.unsafe_type_of env sigma abstr_trm in + let _ = Typing.unsafe_type_of env sigma (EConstr.of_constr abstr_trm) in Sigma.Unsafe.of_pair (applist(abstr_trm, List.map snd loccs_trm), sigma) with Type_errors.TypeError (env',t) -> raise (ReductionTacticError (InvalidAbstraction (env,sigma,abstr_trm,(env',t)))) |