From 62e3a3ce3ac21ab25074ad2af1883a4b0cbc62be Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Mon, 27 Nov 2006 12:54:42 +0000 Subject: [PATCH] Removed a couple of assertions. --- components/tactics/paramodulation/saturation.ml | 2 -- 1 file changed, 2 deletions(-) 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 -- 2.39.2