A few other tactics made available to matita.

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

diff --git a/helm/ocaml/tactics/reductionTactics.ml b/helm/ocaml/tactics/reductionTactics.ml
index 430414b78b8f25376355b126afe3d5a727ce0ae2..bfbfdb2a37c0a1113336f9b2d8dec4339f799859 100644 (file)
--- a/helm/ocaml/tactics/reductionTactics.ml
+++ b/helm/ocaml/tactics/reductionTactics.ml
@@ -125,15 +125,13 @@ let whd_tac ~pattern =
 let normalize_tac ~pattern = 
  mk_tactic (reduction_tac ~reduction:CicReduction.normalize ~pattern );;
 
-let fold_tac ~reduction ~also_in_hypotheses ~term =
- let fold_tac ~reduction ~also_in_hypotheses ~term (proof,goal) =
+let fold_tac ~reduction ~pattern ~term =
+(*
+ let fold_tac ~reduction ~pattern:(hyp_patterns,goal_pattern) ~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
-    (* We don't know if [term] is a subterm of [ty] or a subterm of *)
-    (* the type of one metavariable. So we replace it everywhere.   *)
-    (*CSC: ma si potrebbe ovviare al problema. Ma non credo *)
-    (*CSC: che si guadagni nulla in fatto di efficienza.    *) 
     let replace =
      ProofEngineReduction.replace ~equality:(=) ~what:[term'] ~with_what:[term]
     in
@@ -160,5 +158,6 @@ let fold_tac ~reduction ~also_in_hypotheses ~term =
      in
       (curi,metasenv',pbo,pty), [metano]
  in
-  mk_tactic (fold_tac ~reduction ~also_in_hypotheses ~term)
+  mk_tactic (fold_tac ~reduction ~pattern ~term)
+*) assert false
 ;;