From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Mon, 27 Nov 2006 12:54:42 +0000 (+0000)
Subject: Removed a couple of assertions.
X-Git-Tag: 0.4.95@7852~774
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=62e3a3ce3ac21ab25074ad2af1883a4b0cbc62be;p=helm.git

Removed a couple of assertions.
---

diff --git a/components/tactics/paramodulation/saturation.ml b/components/tactics/paramodulation/saturation.ml
index d9472601c..7ef8d41ac 100644
--- a/components/tactics/paramodulation/saturation.ml
+++ b/components/tactics/paramodulation/saturation.ml
@@ -1531,7 +1531,6 @@ let pump_actives context bag maxm active passive saturation_steps max_time =
   let passive_l = fst passive in
   let ma = max_l active_l in
   let mp = max_l passive_l in
-  assert (maxm > max ma mp);
   match LibraryObjects.eq_URI () with
     | None -> active, passive, !maxmeta
     | Some eq_uri -> 
@@ -1593,7 +1592,6 @@ let given_clause
   let passive_l = fst passive in
   let ma = max_l active_l in
   let mp = max_l passive_l in
-  assert (maxm > max ma mp);
   let proof, goalno = status in
   let uri, metasenv, meta_proof, term_to_prove = proof in
   let _, context, type_of_goal = CicUtil.lookup_meta goalno metasenv in