diff options
| author | delahaye | 2000-07-21 15:26:18 +0000 |
|---|---|---|
| committer | delahaye | 2000-07-21 15:26:18 +0000 |
| commit | 105fdc0794cdb9336262c50068b3d31e7c6e0da7 (patch) | |
| tree | 6768c6e555623d4033310773c6b15e95acff835c /pretyping | |
| parent | 7cd7b7599c2a66a0173b502cd1c54c4e0af80c39 (diff) | |
Modifs d'interpretation de patterns
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@562 85f007b7-540e-0410-9357-904b9bb8a0f7
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 |