diff --git a/src/transform/abstract_quantifiers.ml b/src/transform/abstract_quantifiers.ml
index 4ae305ad3b03ce23ca0ab157013e4d6041a433ee..b6fc919f26997c975134d94b82d5cba4ee2d354b 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@."