All the reduction tactics have been modified to reduce several (sub)terms

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

diff --git a/helm/ocaml/tactics/reductionTactics.ml b/helm/ocaml/tactics/reductionTactics.ml
index 54b439b25ae40ef31a0fc0c8356eadec95774383..b29873a1fceae31c4521c231bfd503ce29b65585 100644 (file)
--- a/helm/ocaml/tactics/reductionTactics.ml
+++ b/helm/ocaml/tactics/reductionTactics.ml
@@ -40,11 +40,11 @@ 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 ~term ~status:(proof,goal) =
+let reduction_tac ~also_in_hypotheses ~reduction ~terms ~status:(proof,goal) =
  let curi,metasenv,pbo,pty = proof in
  let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
-  let term =
-   match term with None -> ty | Some t -> t
+  let terms =
+   match terms with None -> [ty] | Some l -> l
   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.   *)
@@ -57,8 +57,8 @@ let reduction_tac ~also_in_hypotheses ~reduction ~term ~status:(proof,goal) =
 (*CSC: siamo nel contesto errato. Metto il try, ma che schifo!!!!      *)
 (*CSC: Anche perche' cosi' catturo anche quelle del replace che non dovrei *)
    try
-    let term' = reduction context term in
-     ProofEngineReduction.replace ~equality:(==) ~what:term ~with_what:term'
+    let terms' = List.map (reduction context) terms in
+     ProofEngineReduction.replace ~equality:(==) ~what:terms ~with_what:terms'
       ~where:where
    with
     _ -> where
@@ -101,7 +101,7 @@ let fold_tac ~reduction ~also_in_hypotheses ~term ~status:(proof,goal) =
    (*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
+    ProofEngineReduction.replace ~equality:(=) ~what:[term'] ~with_what:[term]
    in
     let ty' = replace ty in
     let metasenv' =