From 9c3d79a02d17d20a433c9784d3438f60faed1d07 Mon Sep 17 00:00:00 2001
From: Nathan Koskas de Diego <nathan.koskasdediego@cea.fr>
Date: Sat, 26 Mar 2022 18:52:29 +0100
Subject: [PATCH] [qed] bug fixes
---
src/plugins/qed/term.ml | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/src/plugins/qed/term.ml b/src/plugins/qed/term.ml
index 935f3729c9f..a903d576c77 100644
--- a/src/plugins/qed/term.ml
+++ b/src/plugins/qed/term.ml
@@ -2306,7 +2306,7 @@ struct
| Lambda, _ -> true
| Forall, x | Exists, x -> Vars.mem x e.vars
) qxs in
- let xs = List.map (fun (_q, x) -> x) qxs in
+ let xs = List.rev_map (fun (_q, x) -> x) qxs in
let e = lc_close_xs xs e in
List.fold_right (fun (q, x) e -> c_bind q (tau_of_var x) e) qxs e
--
GitLab