From 08f4cfc9dfb03973ae652ef6576342ae38f8f199 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Thu, 6 Oct 2016 11:21:10 +0200
Subject: w_merge: Add a comment about the (List.rev evars)

This change exposed bug #4763
---
 pretyping/unification.ml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 3d734ea9a9..b7edd6fcd6 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -1361,7 +1361,9 @@ let w_merge env with_types flags (evd,metas,evars) =
     in w_merge_rec evd [] [] eqns
   in
   let res =  (* merge constraints *)
-    w_merge_rec evd (order_metas metas) (List.rev evars) []
+    w_merge_rec evd (order_metas metas)
+                (* Assign evars in the order of assignments during unification *)
+                (List.rev evars) []
   in
     if with_types then check_types res
     else res
-- 
cgit v1.2.3