Universe.key was not used to index terms, but was used to retrieve them

[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..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
@@ -175,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 =
@@ -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