[Transform] Abstract quantifier abstract also quantifiers in goal

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 []
+  | 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@."