better check for progress

[helm.git] / helm / software / components / tactics / reductionTactics.ml

diff --git a/helm/software/components/tactics/reductionTactics.ml b/helm/software/components/tactics/reductionTactics.ml
index e1bedeb207ff473653f1a06899b14df780b96c0d..8a0d739be6883804d463d25389801a5779d615b0 100644 (file)
--- a/helm/software/components/tactics/reductionTactics.ml
+++ b/helm/software/components/tactics/reductionTactics.ml
@@ -67,17 +67,9 @@ let reduction_tac ~reduction ~pattern (proof,goal) =
           Some (name,Cic.Decl ty')::context', metasenv, ugraph
        | Some (name,Cic.Def (bo,ty)),Some (`Def (selected_bo,selected_ty)) ->
           let bo', metasenv, ugraph =
-            change subst bo selected_bo metasenv ugraph
-          in
+            change subst bo selected_bo metasenv ugraph in
           let ty', metasenv, ugraph =
-           match ty,selected_ty with
-              None,None -> None, metasenv, ugraph
-            | Some ty,Some selected_ty ->
-                let ty', metasenv, ugraph =
-                  change subst ty selected_ty metasenv ugraph
-                in
-                Some ty', metasenv, ugraph
-            | _,_ -> assert false
+            change subst ty selected_ty metasenv ugraph
           in
            (Some (name,Cic.Def (bo',ty'))::context'), metasenv, ugraph
        | _,_ -> assert false
@@ -190,17 +182,9 @@ let change_tac ?(with_cast=false) ~pattern with_what  =
            (Some (name,Cic.Decl ty')::context'), metasenv, ugraph
        | Some (name,Cic.Def (bo,ty)),Some (`Def (selected_bo,selected_ty)) ->
           let bo', metasenv, ugraph =
-            change subst bo selected_bo metasenv ugraph
-          in
+            change subst bo selected_bo metasenv ugraph in
           let ty', metasenv, ugraph =
-           match ty,selected_ty with
-              None,None -> None, metasenv, ugraph
-            | Some ty,Some selected_ty ->
-                let ty', metasenv, ugraph =
-                  change subst ty selected_ty metasenv ugraph
-                in
-                Some ty', metasenv, ugraph
-            | _,_ -> assert false
+            change subst ty selected_ty metasenv ugraph
           in
            (Some (name,Cic.Def (bo',ty'))::context'), metasenv, ugraph
        | _,_ -> assert false