diff options
| -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 10e8cf7e0f..f87c50b5e4 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -1197,7 +1197,7 @@ let abstract_scheme env sigma (locc,a) (c, sigma) = let pattern_occs loccs_trm = begin fun env sigma c -> let abstr_trm, sigma = List.fold_right (abstract_scheme env sigma) loccs_trm (c,sigma) in try - let _ = Typing.unsafe_type_of env sigma abstr_trm in + let sigma, _ = Typing.type_of env sigma abstr_trm in (sigma, applist(abstr_trm, List.map snd loccs_trm)) with Type_errors.TypeError (env',t) -> raise (ReductionTacticError (InvalidAbstraction (env,sigma,abstr_trm,(env',t)))) |