X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2FproofEngineStructuralRules.ml;h=47921953742be893160a5c5751570af6923b1d87;hb=b3e08a6954c8b6946f42f5c7e0bed7912d5ac87c;hp=3f96677b8b01d8bd0e7c5bc07d419b26ccfccd3a;hpb=cc23f034c9419186602d9250456241f2eba90d7c;p=helm.git

diff --git a/helm/software/components/tactics/proofEngineStructuralRules.ml b/helm/software/components/tactics/proofEngineStructuralRules.ml
index 3f96677b8..479219537 100644
--- a/helm/software/components/tactics/proofEngineStructuralRules.ml
+++ b/helm/software/components/tactics/proofEngineStructuralRules.ml
@@ -53,7 +53,7 @@ let clearbody ~hyp =
                      let _,_ =
                       try
                        CicTypeChecker.type_of_aux' metasenv context t
-                        CicUniv.empty_ugraph (* TASSI: FIXME *)
+                        CicUniv.oblivion_ugraph (* TASSI: FIXME *)
                       with
                        _ ->
                          raise
@@ -68,10 +68,10 @@ let clearbody ~hyp =
                      (try
                        ignore
                         (CicTypeChecker.type_of_aux' metasenv context te
-                          CicUniv.empty_ugraph (* TASSI: FIXME *));
+                          CicUniv.oblivion_ugraph (* TASSI: FIXME *));
                        ignore
                         (CicTypeChecker.type_of_aux' metasenv context ty
-                          CicUniv.empty_ugraph (* TASSI: FIXME *));
+                          CicUniv.oblivion_ugraph (* TASSI: FIXME *));
                       with
                        _ ->
                          raise
@@ -86,7 +86,7 @@ let clearbody ~hyp =
               let _,_ =
                try
                 CicTypeChecker.type_of_aux' metasenv canonical_context' ty
-                 CicUniv.empty_ugraph (* TASSI: FIXME *)
+                 CicUniv.oblivion_ugraph (* TASSI: FIXME *)
                with
                 _ ->
                  raise
@@ -130,7 +130,7 @@ let clear_one ~hyp =
                          let _,_ =
                           try
                            CicTypeChecker.type_of_aux' metasenv context t
-                            CicUniv.empty_ugraph
+                            CicUniv.oblivion_ugraph
                           with _ ->
                            raise
                             (PET.Fail
@@ -147,7 +147,7 @@ let clear_one ~hyp =
              let _,_ =
                try
                 CicTypeChecker.type_of_aux' metasenv canonical_context' ty
-                 CicUniv.empty_ugraph 
+                 CicUniv.oblivion_ugraph 
                with _ ->
                 raise (PET.Fail (lazy ("Hypothesis " ^ hyp ^ " occurs in the goal")))
               in