From 7fc3d39ca13a3fcbcb0e7887c458b7002ec245f0 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Bobot?= <francois.bobot@cea.fr>
Date: Mon, 30 Jul 2018 21:36:09 +0200
Subject: [PATCH] [Transform] Abstract quantifier abstract also quantifiers in
 goal

---
 src/transform/abstract_quantifiers.ml | 13 +++++++------
 1 file changed, 7 insertions(+), 6 deletions(-)

diff --git a/src/transform/abstract_quantifiers.ml b/src/transform/abstract_quantifiers.ml
index 4ae305ad3..b6fc919f2 100644
--- a/src/transform/abstract_quantifiers.ml
+++ b/src/transform/abstract_quantifiers.ml
@@ -24,13 +24,14 @@ let rec elim_quant pol f =
 
 let elim_less (d:decl) =
   match d.d_node with
-  | Dprop (Paxiom,_v,t) ->
-    let t = elim_quant true t in
-    if t_equal t t_true then []
-    else
-      [decl_map (fun _ -> t) d]
+  | Dprop (p,_v,t) ->
+      let pol = match p with | Paxiom | Plemma -> true | Pgoal -> false in
+      let t = elim_quant pol t in
+      if p <> Pgoal && t_equal t t_true then []
+      else
+        [decl_map (fun _ -> t) d]
   | _ -> [d]
 
 let () =
   Trans.register_transform "abstract_quantifiers" (Trans.decl elim_less None)
-    ~desc:"abstract@ quantifiers@ in@ the@ axioms@ of@ the@ context@."
+    ~desc:"abstract@ quantifiers@ in@ the@ axioms@ of@ the@ context and the goals@."
-- 
GitLab