diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2005-11-02 13:14:43 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2005-11-02 13:14:43 +0000 |
| commit | c6fa7faebb8d08e3f443457f2259c668559964d0 (patch) | |
| tree | fded18a14fa5ec9f432f72c88df73ee46de1da69 /pretyping | |
| parent | bd1b7790419099bf311039f2ab6abff35e08f8d3 (diff) | |
Correction bug invert_names (cf bug #1031)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7490 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/tacred.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index 654f34e27..117b626ea 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -186,13 +186,14 @@ let invert_name labs l na0 env sigma ref = function match refi with | None -> None | Some ref -> - match reference_opt_value sigma env ref with + try match reference_opt_value sigma env ref with | None -> None | Some c -> let labs',ccl = decompose_lam c in let _, l' = whd_betalet_stack ccl in let labs' = List.map snd labs' in if labs' = labs & l = l' then Some ref else None + with Not_found (* Undefined ref *) -> None else Some ref | Anonymous -> None (* Actually, should not occur *) |