Commented an assertion.

diff --git a/helm/software/components/tactics/paramodulation/equality.ml b/helm/software/components/tactics/paramodulation/equality.ml
index 10a64af19d09a15d762697512ba00de2270a964d..1d798f9dc1a7d8b88867a5bc9fa6bb908a636405 100644 (file)
--- a/helm/software/components/tactics/paramodulation/equality.ml
+++ b/helm/software/components/tactics/paramodulation/equality.ml
@@ -202,7 +202,7 @@ let build_ens uri termlist =
   let obj, _ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
   match obj with
   | Cic.Constant (_, _, _, uris, _) ->
-      assert (List.length uris <= List.length termlist);
+      (* assert (List.length uris <= List.length termlist); *)
       let rec aux = function
         | [], tl -> [], tl
         | (uri::uris), (term::tl) ->