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: make_still_working~6633
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=ca485beacf0458a72a6bd4ea024906f4005c720b;hp=9a537a6b50c60cb80d0dcfb343bf6e68e035842c;p=helm.git

Removed a couple of assertions.
---

diff --git a/helm/software/components/tactics/paramodulation/saturation.ml b/helm/software/components/tactics/paramodulation/saturation.ml
index d9472601c..7ef8d41ac 100644
--- a/helm/software/components/tactics/paramodulation/saturation.ml
+++ b/helm/software/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