From b67fa1d87a1af9a2caa89c2d9eb7f2c0707b4a90 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Tue, 3 Dec 2019 10:39:47 +0100
Subject: [PATCH] [qed] fix rebuild record with single field
---
src/plugins/qed/term.ml | 5 +++--
1 file changed, 3 insertions(+), 2 deletions(-)
diff --git a/src/plugins/qed/term.ml b/src/plugins/qed/term.ml
index 7a2a8774a28..cd515a64e87 100644
--- a/src/plugins/qed/term.ml
+++ b/src/plugins/qed/term.ml
@@ -884,7 +884,7 @@ struct
let c_record fxs =
match fxs with
- | [] | [_] -> insert(Rdef fxs)
+ | [] -> insert(Rdef fxs)
| fx::gys ->
try
let base (f,v) =
@@ -2550,7 +2550,8 @@ struct
| _ -> true)
fvs
in
- Some ( base , fothers )
+ if fothers = [] then None (* suspiscious *)
+ else Some ( base , fothers )
(* ------------------------------------------------------------------------ *)
(* --- Symbol --- *)
--
GitLab