From: denes Date: Tue, 23 Jun 2009 22:46:49 +0000 (+0000) Subject: Removed old debugging assertion X-Git-Tag: make_still_working~3811 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=158c113b8713291b4162f4c76d587bc42cdb25b7;hp=36270146f49052f621553b0b45afe23813ed7e64;p=helm.git Removed old debugging assertion --- diff --git a/helm/software/components/ng_paramodulation/paramod.ml b/helm/software/components/ng_paramodulation/paramod.ml index ec098a615..e747d6693 100644 --- a/helm/software/components/ng_paramodulation/paramod.ml +++ b/helm/software/components/ng_paramodulation/paramod.ml @@ -147,7 +147,6 @@ let nparamod rdb metasenv subst context t table = let bag,maxvar,actives,passives,g_actives,g_passives = aux_select passives g_passives in - assert (PassiveSet.cardinal g_passives < 2); debug (Printf.sprintf "Number of active goals : %d" (List.length g_actives));