diff options
author | Enrico Tassi <Enrico.Tassi@inria.fr> | 2018-04-27 14:46:18 +0200 |
---|---|---|
committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2018-04-27 14:46:18 +0200 |
commit | b9c8bb1621e017e029e87bc684255eae775718fc (patch) | |
tree | 388f86e2ec0342cca25a9fe68e3170c8fde5360c | |
parent | 53fb4203b80da48e2ac9b06803c57e81df702a0a (diff) | |
parent | 10a6452c6bbf618428591d9c40aed945f7fe92b3 (diff) |
Merge PR #7358: Fix #7356: missing lift when interpreting default instances of evars
-rw-r--r-- | pretyping/pretyping.ml | 2 | ||||
-rw-r--r-- | test-suite/success/evars.v | 5 |
2 files changed, 6 insertions, 1 deletions
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 947469ca0..e68a25a87 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -1118,7 +1118,7 @@ and pretype_instance k0 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.ExtraEnv.env !evdref t t' then mkRel n, update else raise Not_found + if is_conv env.ExtraEnv.env !evdref t (lift n t') then mkRel n, update else raise Not_found with Not_found -> try let t' = env |> lookup_named id |> NamedDecl.get_type in diff --git a/test-suite/success/evars.v b/test-suite/success/evars.v index 5b13f35d5..253b48e4d 100644 --- a/test-suite/success/evars.v +++ b/test-suite/success/evars.v @@ -421,3 +421,8 @@ Goal exists n : nat, n = n -> True. eexists. set (H := _ = _). Abort. + +(* Check interpretation of default evar instance in pretyping *) +(* (reported as bug #7356) *) + +Check fun (P : nat -> Prop) (x:nat) (h:P x) => exist _ ?[z] (h : P ?z). |