diff options
| -rw-r--r-- | pretyping/instantiate.ml | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/pretyping/instantiate.ml b/pretyping/instantiate.ml index 42a4dbba7b..95ce7b6bfc 100644 --- a/pretyping/instantiate.ml +++ b/pretyping/instantiate.ml @@ -44,7 +44,10 @@ let instantiate_evar sign c args = (* Existentials. *) let existential_type sigma (n,args) = - let info = Evd.map sigma n in + let info = + try Evd.map sigma n + with Not_found -> + anomaly ("Evar ?"^string_of_int n^" was not declared") in let hyps = info.evar_hyps in instantiate_evar hyps info.evar_concl (Array.to_list args) |