From c12e158ad85da9d5e78026997ef6ca969c8ad3a6 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 17 Oct 2016 19:32:23 +0200
Subject: Fixing a missing constraint in consider_remaining_unif_constraints.

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

diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 0d261f7f87..d82d555f84 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -1130,7 +1130,7 @@ let apply_conversion_problem_heuristic ts env evd pbty t1 t2 =
       let f env evd pbty x y = is_trans_fconv pbty ts env evd x y in
       Success (solve_refl ~can_drop:true f env evd
                  (position_problem true pbty) evk1 args1 args2)
-  | Evar ev1, Evar ev2 ->
+  | Evar ev1, Evar ev2 when app_empty ->
       Success (solve_evar_evar ~force:true
         (evar_define (evar_conv_x ts) ~choose:true) (evar_conv_x ts) env evd
         (position_problem true pbty) ev1 ev2)
-- 
cgit v1.2.3