diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-11-03 20:13:38 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-11-03 20:43:16 +0100 |
| commit | 71c56620314bc28c6d7a643a2174518e74da6d50 (patch) | |
| tree | 1d0093869a748e70027a4778104e29fecb958541 /pretyping/pretyping.ml | |
| parent | 06b6a53bbc16ac2fd53213d693910c73105564c5 (diff) | |
Fixing confused code for interpretations of evar instances.
Diffstat (limited to 'pretyping/pretyping.ml')
| -rw-r--r-- | pretyping/pretyping.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 88a10352a..16d92ad78 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -907,11 +907,11 @@ and pretype_instance resolve_tc env evdref lvar loc hyps evk update = with Not_found -> try let (n,_,t') = lookup_rel_id id (rel_context env) in - if is_conv env !evdref t t' then raise Not_found else mkRel n, update + if is_conv env !evdref t t' then mkRel n, update else raise Not_found with Not_found -> try let (_,_,t') = lookup_named id env in - if is_conv env !evdref t t' then raise Not_found else mkVar id, update + if is_conv env !evdref t t' then mkVar id, update else raise Not_found with Not_found -> user_err_loc (loc,"",str "Cannot interpret " ++ pr_existential_key !evdref evk ++ |