Demodulate used to be a reduction_kind and it used to take a ~pattern.

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

diff --git a/helm/software/components/tactics/paramodulation/saturation.ml b/helm/software/components/tactics/paramodulation/saturation.ml
index cbf15f0dfdad34e6e26a8f2ba4e532c713812f79..6cd2bcf4a8240813ef0bdf520902576d69369fb8 100644 (file)
--- 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)))