X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2FproofEngineStructuralRules.ml;h=3b8b6f92c933c89b01ee7e264dae952ed9436be2;hb=7e9904185ceff75884783dbf0bad506b8521b857;hp=e8956944528197c456992eb72d1dae5e777701a3;hpb=655906d74521fa49de332f54ec34bfc9d9744151;p=helm.git

diff --git a/helm/ocaml/tactics/proofEngineStructuralRules.ml b/helm/ocaml/tactics/proofEngineStructuralRules.ml
index e89569445..3b8b6f92c 100644
--- a/helm/ocaml/tactics/proofEngineStructuralRules.ml
+++ b/helm/ocaml/tactics/proofEngineStructuralRules.ml
@@ -50,8 +50,9 @@ let clearbody ~hyp =
                      match entry with
                         t when t == hyp_to_clear_body ->
                          let cleared_entry =
-                          let ty =
+                          let ty,_ =
                            CicTypeChecker.type_of_aux' metasenv context term
+			     CicUniv.empty_ugraph (* TASSI: FIXME *)
                           in
                            Some (n_to_clear_body, Cic.Decl ty)
                          in
@@ -59,9 +60,10 @@ let clearbody ~hyp =
                       | None -> None::context
                       | Some (n,C.Decl t)
                       | Some (n,C.Def (t,None)) ->
-                         let _ =
+                         let _,_ =
                           try
                            CicTypeChecker.type_of_aux' metasenv context t
+			     CicUniv.empty_ugraph (* TASSI: FIXME *)
                           with
                            _ ->
                              raise
@@ -76,9 +78,10 @@ let clearbody ~hyp =
                       | Some (_,Cic.Def (_,Some _)) -> assert false
                    ) canonical_context []
                  in
-                  let _ =
+                  let _,_ =
                    try
                     CicTypeChecker.type_of_aux' metasenv canonical_context' ty
+		      CicUniv.empty_ugraph (* TASSI: FIXME *)
                    with
                     _ ->
                      raise
@@ -122,9 +125,10 @@ let clear ~hyp =
                       | Some (_,Cic.Def (_,Some _)) -> assert false
                       | Some (n,C.Decl t)
                       | Some (n,C.Def (t,None)) ->
-                         let _ =
+                         let _,_ =
                           try
                            CicTypeChecker.type_of_aux' metasenv context t
+			     CicUniv.empty_ugraph (* TASSI: FIXME *)
                           with
                            _ ->
                              raise
@@ -138,9 +142,10 @@ let clear ~hyp =
                           entry::context
                    ) canonical_context []
                  in
-                  let _ =
+                  let _,_ =
                    try
                     CicTypeChecker.type_of_aux' metasenv canonical_context' ty
+		      CicUniv.empty_ugraph (* TASSI: FIXME *)
                    with
                     _ ->
                      raise