Added universes handling. The PRE_UNIVERSES tag may help ;)

[helm.git] / helm / ocaml / tactics / proofEngineStructuralRules.ml

diff --git a/helm/ocaml/tactics/proofEngineStructuralRules.ml b/helm/ocaml/tactics/proofEngineStructuralRules.ml
index e8956944528197c456992eb72d1dae5e777701a3..3b8b6f92c933c89b01ee7e264dae952ed9436be2 100644 (file)
--- 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