From ca485beacf0458a72a6bd4ea024906f4005c720b 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. --- helm/software/components/tactics/paramodulation/saturation.ml | 2 -- 1 file changed, 2 deletions(-) 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 -- 2.39.5