diff options
| author |  Stephane Glondu <steph@glondu.net> | 2010-10-14 17:51:11 +0200 |
|---|---|---|
| committer | Stephane Glondu <steph@glondu.net> | 2010-10-14 17:51:11 +0200 |
| commit | 3e96002677226c0cdaa8f355938a76cfb37a722a (patch) | |
| tree | 3ca96e142fdb68e464d2f5f403f315282b94f922 /pretyping/pretyping.ml | |
| parent | f18e6146f4fd6ed5b8ded10a3e602f5f64f919f4 (diff) | |
Imported Upstream version 8.3upstream/8.3
Diffstat (limited to 'pretyping/pretyping.ml')
| -rw-r--r-- | pretyping/pretyping.ml | 9 |
1 files changed, 7 insertions, 2 deletions
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 7b4b5e07..1c17ff88 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: pretyping.ml 13332 2010-07-26 22:12:43Z msozeau $ *) +(* $Id: pretyping.ml 13408 2010-09-11 19:19:04Z herbelin $ *) open Pp open Util @@ -235,6 +235,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 = try let (n,_,typ) = lookup_rel_id id (rel_context env) in @@ -244,7 +249,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 -> try let (_,_,typ) = lookup_named id env in |