From 82b371aceb1ef6b1e15bdace2cf142e65724a3c6 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Thu, 17 Mar 2016 17:53:25 +0100
Subject: Fix #4623: set tactic too weak with universes (regression)

The regression was introduced by efa1c32a4d178, which replaced
unification by conversion when looking for more occurrences of a
subterm. The conversion function called was not the right one, as it
was not inferring constraints.
---
 pretyping/unification.ml | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 9b6e856b80..cd0bbfa300 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -1532,8 +1532,9 @@ let make_pattern_test from_prefix_of_ind is_correct_type env sigma (pending,c) =
     | e when Errors.noncritical e -> raise (NotUnifiable None) in
   let merge_fun c1 c2 =
     match c1, c2 with
-    | Some (evd,c1,_) as x, Some (_,c2,_) ->
-      if is_conv env sigma c1 c2 then x else raise (NotUnifiable None)
+    | Some (evd,c1,x), Some (_,c2,_) ->
+      let (evd,b) = infer_conv ~pb:CONV env evd c1 c2 in
+      if b then Some (evd, c1, x) else raise (NotUnifiable None)
     | Some _, None -> c1
     | None, Some _ -> c2
     | None, None -> None in
-- 
cgit v1.2.3