diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/pretyping.ml | 1 | ||||
| -rw-r--r-- | pretyping/retyping.ml | 5 |
2 files changed, 5 insertions, 1 deletions
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 4e658787d0..68a75ee32d 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -462,6 +462,7 @@ let unsafe_fmachine tycon nocheck isevars metamap env lvar lmeta constr = reset_problems (); pretype tycon env isevars lvar lmeta constr + let unsafe_fmachine_type valcon nocheck isevars metamap env lvar lmeta constr = trad_metamap := metamap; trad_nocheck := nocheck; diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml index 72cd94c1dc..60647a946c 100644 --- a/pretyping/retyping.ml +++ b/pretyping/retyping.ml @@ -44,7 +44,10 @@ let rec type_of env cstr= (try strip_outer_cast (List.assoc n metamap) with Not_found -> anomaly "type_of: this is not a well-typed term") | IsRel n -> lift n (body_of_type (snd (lookup_rel n env))) - | IsVar id -> body_of_type (snd (lookup_var id env)) + | IsVar id -> + (try body_of_type (snd (lookup_var id env)) + with Not_found -> + anomaly ("type_of: variable "^(string_of_id id)^" unbound")) | IsAbst _ -> error "No more Abst" (*type_of env (abst_value cstr)*) | IsConst c -> body_of_type (type_of_constant env sigma c) | IsEvar _ -> type_of_existential env sigma cstr |