X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Fparamodulation%2Fsaturation.ml;h=6cd2bcf4a8240813ef0bdf520902576d69369fb8;hb=8752fac73a864c821b6954f0572bce2052924183;hp=cbf15f0dfdad34e6e26a8f2ba4e532c713812f79;hpb=a004949b379723275993bbbda15b004908572871;p=helm.git

diff --git a/helm/software/components/tactics/paramodulation/saturation.ml b/helm/software/components/tactics/paramodulation/saturation.ml
index cbf15f0df..6cd2bcf4a 100644
--- a/helm/software/components/tactics/paramodulation/saturation.ml
+++ b/helm/software/components/tactics/paramodulation/saturation.ml
@@ -1873,7 +1873,7 @@ let main_demod_equalities dbd term metasenv ugraph =
 *)
 ;;
 
-let demodulate_tac ~dbd ~pattern ((proof,goal)(*s initialstatus*)) = 
+let demodulate_tac ~dbd ((proof,goal)(*s initialstatus*)) = 
   let curi,metasenv,pbo,pty = proof in
   let metano,context,ty = CicUtil.lookup_meta goal metasenv in
   let eq_uri = eq_of_goal ty in 
@@ -1917,13 +1917,11 @@ let demodulate_tac ~dbd ~pattern ((proof,goal)(*s initialstatus*)) =
   else (* if newty = ty then *)
     raise (ProofEngineTypes.Fail (lazy "no progress"))
   (*else ProofEngineTypes.apply_tactic 
-    (ReductionTactics.simpl_tac ~pattern) 
-    initialstatus*)
+    (ReductionTactics.simpl_tac
+      ~pattern:(ProofEngineTypes.conclusion_pattern None)) initialstatus*)
 ;;
 
-let demodulate_tac ~dbd ~pattern = 
-  ProofEngineTypes.mk_tactic (demodulate_tac ~dbd ~pattern)
-;;
+let demodulate_tac ~dbd = ProofEngineTypes.mk_tactic (demodulate_tac ~dbd);;
 
 let rec find_in_ctx i name = function
   | [] -> raise (ProofEngineTypes.Fail (lazy ("Hypothesis not found: " ^ name)))