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 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'pretyping') 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 -- cgit v1.2.3