diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/pretyping.ml | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 8898e5989a..7017edaf28 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -249,6 +249,11 @@ module Pretyping_F (Coercion : Coercion.S) = struct str " depends on pattern variable name " ++ pr_id id ++ str " which is not bound in current context.") + let protected_get_type_of env sigma c = + try Retyping.get_type_of env sigma c + with Anomaly _ -> + errorlabstrm "" (str "Cannot reinterpret " ++ quote (print_constr c) ++ str " in the current environment.") + let pretype_id loc env sigma (lvar,unbndltacvars) id = (* Look for the binder of [id] *) try @@ -260,7 +265,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct let (ids,c) = List.assoc id lvar in let subst = List.map (invert_ltac_bound_name env id) ids in let c = substl subst c in - { uj_val = c; uj_type = Retyping.get_type_of env sigma c } + { uj_val = c; uj_type = protected_get_type_of env sigma c } with Not_found -> (* Check if [id] is a section or goal variable *) try |