X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matitaB%2Fcomponents%2Fng_paramodulation%2Fparamod.ml;h=a1ec9bc14caad983ee84a5f80a8467ef88f65ac4;hb=647504aa72b84eb49be8177b88a9254174e84d4b;hp=83845673b3142cf1805323034983fc316bf957c1;hpb=4f3b04e9966484011328d5b0eb358da4416e29b0;p=helm.git diff --git a/matitaB/components/ng_paramodulation/paramod.ml b/matitaB/components/ng_paramodulation/paramod.ml index 83845673b..a1ec9bc14 100644 --- a/matitaB/components/ng_paramodulation/paramod.ml +++ b/matitaB/components/ng_paramodulation/paramod.ml @@ -224,7 +224,7 @@ module Paramod (B : Orderings.Blob) = struct let initialize_goal (bag,maxvar,actives,passives,_,_) t = let (bag,maxvar), g = mk_unit_clause bag maxvar t in let g_passives = g_passive_empty_set in - (* if the goal is not an equation we returns an empty + (* if the goal is not an equation we return an empty passive set *) let g_passives = if Terms.is_eq_clause g then add_passive_goal g_passives g