From d50c25ca21b9fab6da6301201fed5be32449f88f Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 9 Dec 2014 17:44:57 +0100
Subject: Fixing orientation of postponed subtyping problems. In the case of
 conversion, postponing by preserving the initial orientation.

Was wrong from its initial version in Jan 2014, but was not visible
because evar-evar subtyping was approximated by evar-evar conversion.

Thanks to Enrico for a very short example highlighting the problem. In
particular, this fixes Ergo.
---
 pretyping/evarsolve.ml     | 4 ++--
 test-suite/success/evars.v | 4 ++++
 2 files changed, 6 insertions(+), 2 deletions(-)

diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index d0a7e39822..cb5673c2ea 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -120,9 +120,9 @@ let test_success conv_algo env evd c c' rhs =
 
 let add_conv_oriented_pb (pbty,env,t1,t2) evd =
   match pbty with
-  | Some true -> add_conv_pb (Reduction.CUMUL,env,t2,t1) evd
+  | Some true -> add_conv_pb (Reduction.CUMUL,env,t1,t2) evd
   | Some false -> add_conv_pb (Reduction.CUMUL,env,t2,t1) evd
-  | None -> add_conv_pb (Reduction.CONV,env,t2,t1) evd
+  | None -> add_conv_pb (Reduction.CONV,env,t1,t2) evd
 
 (*------------------------------------*
  * Restricting existing evars         *
diff --git a/test-suite/success/evars.v b/test-suite/success/evars.v
index 21c72475ed..f42c6a036e 100644
--- a/test-suite/success/evars.v
+++ b/test-suite/success/evars.v
@@ -404,3 +404,7 @@ Abort.
    not strict enough evar restriction) *)
 
 Check match Some _ with None => _ | _ => _ end.
+
+(* Used to fail for a couple of days in Nov 2014 *)
+
+Axiom test : forall P1 P2, P1 = P2 -> P1 -> P2.
-- 
cgit v1.2.3