Ported innermost strategy for demodulation from trunk

[helm.git] / helm / software / components / ng_paramodulation / nCicParamod.ml

diff --git a/helm/software/components/ng_paramodulation/nCicParamod.ml b/helm/software/components/ng_paramodulation/nCicParamod.ml
index ff34709e9c7a262453de6a124ba6e641919b11b6..2b52ce34a29bc50ef15beb831af87eba1124071f 100644 (file)
--- a/helm/software/components/ng_paramodulation/nCicParamod.ml
+++ b/helm/software/components/ng_paramodulation/nCicParamod.ml
@@ -94,7 +94,3 @@ let nparamod rdb metasenv subst context (g_t,g_ty) table =
       proofterm, metasenv, subst)
     solutions
 ;;
-  
-  
-
-