From 97329e9fef5a13d017a285d935b242c1968aab2b Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Thu, 20 Apr 2023 11:18:23 +0200
Subject: [PATCH] [kernel] don't forget to instantiate variables before using
types
---
src/kernel_services/ast_queries/logic_typing.ml | 6 +++++-
1 file changed, 5 insertions(+), 1 deletion(-)
diff --git a/src/kernel_services/ast_queries/logic_typing.ml b/src/kernel_services/ast_queries/logic_typing.ml
index 32d75ff5d32..be6367396e2 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
--
GitLab