From 9b9074640c23ced68d92f75558caa2ed77770bcc Mon Sep 17 00:00:00 2001
From: Hugo Herbelin <Hugo.Herbelin@inria.fr>
Date: Tue, 12 Jun 2018 12:16:40 +0200
Subject: Fixes #7780 (missing lift in expanding alias under a binder in
 unification).

---
 pretyping/evarsolve.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'pretyping')

diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index aefae1ecc..8afb9b942 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -929,7 +929,7 @@ let invert_arg_from_subst evd aliases k0 subst_in_env_extended_with_k_binders c_
     with Not_found ->
       match expand_alias_once evd aliases t with
       | None -> raise Not_found
-      | Some c -> aux k c in
+      | Some c -> aux k (lift k c) in
   try
     let c = aux 0 c_in_env_extended_with_k_binders in
     Invertible (UniqueProjection (c,!effects))
-- 
cgit v1.2.3