demodulate takes an extra argument 'all', if present it attempts to solve

[helm.git] / helm / software / components / tactics / paramodulation / utils.ml

diff --git a/helm/software/components/tactics/paramodulation/utils.ml b/helm/software/components/tactics/paramodulation/utils.ml
index 8a2722bb6820a1bf3d06652c8d9101be147dabad..86c9c1430105e0948c4ba3274284b9b9b03caded 100644 (file)
--- a/helm/software/components/tactics/paramodulation/utils.ml
+++ b/helm/software/components/tactics/paramodulation/utils.ml
@@ -25,7 +25,7 @@
 
 (* $Id$ *)
 
-let time = true;;
+let time = false;;
 let debug = false;;
 let debug_metas = false;; 
 let debug_res = false;;
@@ -114,6 +114,8 @@ let rec remove_local_context =
     | Cic.Meta (i,_) -> Cic.Meta (i,[])
     | Cic.Appl l ->
        Cic.Appl(List.map remove_local_context l)
+    | Cic.Prod (n,s,t) -> 
+       Cic.Prod (n,remove_local_context s, remove_local_context t)
     | t -> t