more abstract discrimination tree

[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 f8e613723ff25eb69924d1e209f0bf14c258a2fb..c943e7a19cafdf592426615182dfdd5cdd4bdf07 100644 (file)
--- a/helm/software/components/tactics/reductionTactics.ml
+++ b/helm/software/components/tactics/reductionTactics.ml
@@ -51,7 +51,7 @@ let reduction_tac ~reduction ~pattern (proof,goal) =
      CicMetaSubst.apply_subst subst where', metasenv, ugraph
   in
   let (subst,metasenv,ugraph,selected_context,selected_ty) =
-    ProofEngineHelpers.select ~metasenv ~ugraph:CicUniv.empty_ugraph
+    ProofEngineHelpers.select ~metasenv ~ugraph:CicUniv.oblivion_ugraph
       ~conjecture ~pattern
   in
   let ty', metasenv, ugraph = change subst ty selected_ty metasenv ugraph in
@@ -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
@@ -102,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)
   
@@ -165,7 +167,7 @@ let change_tac ?(with_cast=false) ~pattern with_what  =
       CicMetaSubst.apply_subst subst where', metasenv, ugraph
   in
   let (subst,metasenv,ugraph,selected_context,selected_ty) =
-   ProofEngineHelpers.select ~metasenv ~ugraph:CicUniv.empty_ugraph ~conjecture
+   ProofEngineHelpers.select ~metasenv ~ugraph:CicUniv.oblivion_ugraph ~conjecture
     ~pattern in
   let ty', metasenv, ugraph = change subst ty selected_ty metasenv ugraph in
   let context', metasenv, ugraph =
@@ -180,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