From 10a6452c6bbf618428591d9c40aed945f7fe92b3 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 26 Apr 2018 14:45:45 +0200
Subject: Pretyping: Fixing a de Bruijn bug in interpreting default instances
 of evars.

---
 pretyping/pretyping.ml     | 2 +-
 test-suite/success/evars.v | 5 +++++
 2 files changed, 6 insertions(+), 1 deletion(-)

diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 947469ca0e..e68a25a873 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 5b13f35d57..253b48e4d9 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).
-- 
cgit v1.2.3