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 +-
 test-suite/bugs/closed/7780.v | 16 ++++++++++++++++
 2 files changed, 17 insertions(+), 1 deletion(-)
 create mode 100644 test-suite/bugs/closed/7780.v

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))
diff --git a/test-suite/bugs/closed/7780.v b/test-suite/bugs/closed/7780.v
new file mode 100644
index 000000000..2318f4d6e
--- /dev/null
+++ b/test-suite/bugs/closed/7780.v
@@ -0,0 +1,16 @@
+(* A lift was missing in expanding aliases under binders for unification *)
+
+(* Below, the lift was missing while expanding the reference to
+   [mkcons] in [?N] which was under binder [arg] *)
+
+Goal forall T (t : T) (P P0 : T -> Set), option (option (list (P0 t)) -> option (list (P t))).
+  intros ????.
+  refine (Some
+            (fun rls
+             => let mkcons := ?[M] in
+                let default arg := ?[N] in
+                match rls as rls (* 2 *) return option (list (P ?[O])) with
+                | Some _ => None
+                | None => None
+                end)).
+Abort.
-- 
cgit v1.2.3