X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2FreductionTactics.ml;h=bfbfdb2a37c0a1113336f9b2d8dec4339f799859;hb=6a9d597352e104434a1a7f371fdd1bbdac5e50a3;hp=430414b78b8f25376355b126afe3d5a727ce0ae2;hpb=f85e6f52232af229b80a8447492cfae80f95d832;p=helm.git

diff --git a/helm/ocaml/tactics/reductionTactics.ml b/helm/ocaml/tactics/reductionTactics.ml
index 430414b78..bfbfdb2a3 100644
--- 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
 ;;