X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2FreductionTactics.ml;h=8a0d739be6883804d463d25389801a5779d615b0;hb=385fe4ef8b24dc17d2c6a214c9b025c5275f1d7e;hp=9c39caa6f4cee2a4f03fbf505591398a65c24fda;hpb=73993c770d613df679df63d8d3d89fc37c02ae09;p=helm.git

diff --git a/helm/software/components/tactics/reductionTactics.ml b/helm/software/components/tactics/reductionTactics.ml
index 9c39caa6f..8a0d739be 100644
--- 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
@@ -95,10 +87,6 @@ let simpl_tac ~pattern =
  mk_tactic (reduction_tac
   ~reduction:(const_lazy_reduction ProofEngineReduction.simpl) ~pattern)
 
-let reduce_tac ~pattern =
- mk_tactic (reduction_tac
-  ~reduction:(const_lazy_reduction ProofEngineReduction.reduce) ~pattern)
-
 let unfold_tac what ~pattern =
   let reduction =
     match what with
@@ -106,7 +94,17 @@ let unfold_tac what ~pattern =
     | Some lazy_term ->
         (fun context metasenv ugraph ->
           let what, metasenv, ugraph = lazy_term context metasenv ugraph in
-          ProofEngineReduction.unfold ~what, metasenv, ugraph)
+          let unfold ctx t =
+           try
+            ProofEngineReduction.unfold ~what ctx t
+           with
+            (* Not what we would like to have; however, this is required
+               right now for the case of a definition in the context:
+               if it works only in the body (or only in the type), that should
+               be accepted *)
+            ProofEngineTypes.Fail _ -> t
+          in
+          unfold, metasenv, ugraph)
   in
   mk_tactic (reduction_tac ~reduction ~pattern)
   
@@ -184,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