diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-11-06 17:21:44 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-02-14 17:25:30 +0100 |
| commit | e27949240f5b1ee212e7d0fe3326a21a13c4abb0 (patch) | |
| tree | bf076ea31e6ca36cc80e0f978bc63d112e183725 /pretyping/tacred.ml | |
| parent | b365304d32db443194b7eaadda63c784814f53f1 (diff) | |
Typing API using EConstr.
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)))) |