From a420b45b3a4ff853fc6abc2f1fc292479109b7cc Mon Sep 17 00:00:00 2001
From: Nathan Koskas de Diego <nathan.koskasdediego@cea.fr>
Date: Mon, 9 May 2022 12:34:17 +0200
Subject: [PATCH] [Qed] small changes + bug fix
---
src/plugins/qed/term.ml | 9 ++++-----
1 file changed, 4 insertions(+), 5 deletions(-)
diff --git a/src/plugins/qed/term.ml b/src/plugins/qed/term.ml
index 92283dae679..1d6bae3b1a6 100644
--- a/src/plugins/qed/term.ml
+++ b/src/plugins/qed/term.ml
@@ -2324,7 +2324,7 @@ struct
) qxs in
let rxs = List.map (fun (_q, x) -> x) qxs in
let e = lc_close_xs ~reversed:true rxs e in
- List.fold_right (fun (q, x) e -> c_bind q (tau_of_var x) e) qxs e
+ List.fold_left (fun e (q, x) -> c_bind q (tau_of_var x) e) e qxs
let rec subst sigma alpha e =
if filter sigma e then
@@ -2563,9 +2563,8 @@ struct
if changed then aux e xs else e, xs
in
let e, xs = aux e xs in
- let rxs = List.rev xs in
- let e = lc_close_xs ~reversed:true rxs e in
- List.fold_left (fun e x -> c_bind q (tau_of_var x) e) e rxs
+ let e = lc_close_xs ~reversed:false xs e in
+ List.fold_right (fun x e -> c_bind q (tau_of_var x) e) xs e
let e_forall = bind_xs Forall
let e_exists = bind_xs Exists
@@ -2581,7 +2580,7 @@ struct
if changed then aux e else e
in
let e = aux e in
- let rxs = List.sort (fun x y -> -(POOL.compare x y)) (Vars.elements e.vars) in
+ let rxs = List.sort (fun x y -> POOL.compare y x) (Vars.elements e.vars) in
let e = lc_close_xs ~subset:true ~reversed:true rxs e in
List.fold_left (fun e x -> c_bind q (tau_of_var x) e) e rxs
--
GitLab