From 7cf52f22a25ea83c3f965acb50249f737482473a Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Tue, 24 May 2022 16:27:35 +0200
Subject: [PATCH] [qed] remove useless optional flag
---
src/plugins/qed/term.ml | 3 ++-
1 file changed, 2 insertions(+), 1 deletion(-)
diff --git a/src/plugins/qed/term.ml b/src/plugins/qed/term.ml
index 1d6bae3b1a6..dfc55d03fc7 100644
--- a/src/plugins/qed/term.ml
+++ b/src/plugins/qed/term.ml
@@ -2162,7 +2162,8 @@ struct
(* Alpha-convert free-variables in xs with the top-most bound variables *)
(* Only activate flag subset if lc.vars is a subset of xs *)
- let lc_close_xs ?(subset = false) ?(reversed = false) xs (lc : lc_term) : lc_term =
+ (* Warning: ~reversed:false needs to compute the length of xs *)
+ let lc_close_xs ?(subset = false) ~reversed xs (lc : lc_term) : lc_term =
let mu = cache () in
begin
if reversed then
--
GitLab