reverted to ==

diff --git a/helm/ocaml/tactics/reductionTactics.ml b/helm/ocaml/tactics/reductionTactics.ml
index decb161f60ebb3533e8b2e978f706d0d77b8940b..d356499a1d50fccad761e5c7ed7d3adb8d2ae6f6 100644 (file)
--- a/helm/ocaml/tactics/reductionTactics.ml
+++ b/helm/ocaml/tactics/reductionTactics.ml
@@ -43,10 +43,10 @@ let reduction_tac ~reduction (proof,goal) =
 
 (* The default of term is the thesis of the goal to be prooved *)
 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 curi,metasenv,pbo,pty = proof in
+ let metano,context,ty = CicUtil.lookup_meta goal metasenv in
   let terms =
-    match terms with None -> [ty] | Some l -> l
+   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.   *)
@@ -54,39 +54,32 @@ let reduction_tac ~also_in_hypotheses ~reduction ~terms (proof,goal) =
   (*CSC: sappiamo neppure quale sia il suo contesto!!!! Insomma,  *)
   (*CSC: e' meglio prima cercare il termine e scoprirne il        *)
   (*CSC: contesto, poi ridurre e infine rimpiazzare.              *)
-  let replace lift context where=
-    (*CSC: Per il momento se la riduzione fallisce significa solamente che    *)
-    (*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 terms = List.fold_left 
-        (fun acc t -> 
-            try
-              (CicSubstitution.delift lift t) :: acc
-            with Failure _ -> acc
-        ) [] terms
-      in 
-      let terms' = List.map (reduction context) terms in
-      ProofEngineReduction.replace 
-        ~equality:(=) ~what:terms ~with_what:terms' ~where:where
-     with
-      _ -> where
+   let replace context where=
+(*CSC: Per il momento se la riduzione fallisce significa solamente che *)
+(*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 terms' = List.map (reduction context) terms in
+     ProofEngineReduction.replace ~equality:(==) ~what:terms ~with_what:terms'
+      ~where:where
+   with
+    _ -> where
    in
-   let ty' = replace 0 context ty in
-   let context', _ =
+    let ty' = replace context ty in
+    let context' =
      if also_in_hypotheses then
       List.fold_right
-       (fun entry (context,i) ->
+       (fun entry context ->
          match entry with
-          | Some (name,Cic.Def (t,None)) ->
-             (Some (name,Cic.Def ((replace i context t),None)))::context, i-1
+            Some (name,Cic.Def (t,None)) ->
+             (Some (name,Cic.Def ((replace context t),None)))::context
           | Some (name,Cic.Decl t) ->
-             (Some (name,Cic.Decl (replace i context t)))::context, i-1
-          | None -> None::context, i-1
+             (Some (name,Cic.Decl (replace context t)))::context
+          | None -> None::context
           | Some (_,Cic.Def (_,Some _)) -> assert false
-       ) context ([],(List.length context))
+       ) context []
      else
-      context, 0
+      context
     in
      let metasenv' = 
       List.map