got rid of ~status label so that tactics can now be applied partially,

[helm.git] / helm / ocaml / tactics / reductionTactics.ml

diff --git a/helm/ocaml/tactics/reductionTactics.ml b/helm/ocaml/tactics/reductionTactics.ml
index 5a567b84aa75e6056814d845ea1a35e6d81a6120..80cb3306a18b79a4c08e1c8b40e9625014f86c9e 100644 (file)
--- a/helm/ocaml/tactics/reductionTactics.ml
+++ b/helm/ocaml/tactics/reductionTactics.ml
@@ -24,7 +24,7 @@
  *)
 
 (*
-let reduction_tac ~reduction ~status:(proof,goal) =
+let reduction_tac ~reduction (proof,goal) =
  let curi,metasenv,pbo,pty = proof in
  let metano,context,ty = CicUtil.lookup_meta goal metasenv in
   let new_ty = reduction context ty in
@@ -40,7 +40,7 @@ let reduction_tac ~reduction ~status:(proof,goal) =
 *)
 
 (* The default of term is the thesis of the goal to be prooved *)
-let reduction_tac ~also_in_hypotheses ~reduction ~terms ~status:(proof,goal) =
+let reduction_tac ~also_in_hypotheses ~reduction ~terms (proof,goal) =
  let curi,metasenv,pbo,pty = proof in
  let metano,context,ty = CicUtil.lookup_meta goal metasenv in
   let terms =
@@ -93,7 +93,7 @@ let simpl_tac = reduction_tac ~reduction:ProofEngineReduction.simpl ;;
 let reduce_tac = reduction_tac ~reduction:ProofEngineReduction.reduce ;;
 let whd_tac = reduction_tac ~reduction:CicReduction.whd ;;
 
-let fold_tac ~reduction ~also_in_hypotheses ~term ~status:(proof,goal) =
+let fold_tac ~reduction ~also_in_hypotheses ~term (proof,goal) =
  let curi,metasenv,pbo,pty = proof in
  let metano,context,ty = CicUtil.lookup_meta goal metasenv in
   let term' = reduction context term in