diff --git a/src/kernel_services/ast_queries/logic_typing.ml b/src/kernel_services/ast_queries/logic_typing.ml
index 32d75ff5d3280078fa4a623d66aa5401850d2ce9..be6367396e240900c8403f15de042fe721c8290e 100644
--- a/src/kernel_services/ast_queries/logic_typing.ml
+++ b/src/kernel_services/ast_queries/logic_typing.ml
@@ -1896,7 +1896,11 @@ struct
     let env,ty1,_ =
       partial_unif ~overloaded:false loc t1 t1.term_type var env
     in
-    let rt = conditional_conversion loc rel t1 t2 in
+    let rt =
+      conditional_conversion loc rel
+        { t1 with term_type = ty1 }
+        { t2 with term_type = ty2 }
+    in
     env,rt,ty1,ty2
 
   type conversion = NoConv | ArithConv | IntegralConv | PointerConv