X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FlogicalOperations.ml;h=3fab938a058360d73f93c9d9dcf4ec6b2892af72;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=93c511f138336469b9bb5b3e9cc046effc9dd69f;hpb=e626927b4c1c77bdcd6b545203a0a9c17a9ff136;p=helm.git

diff --git a/helm/gTopLevel/logicalOperations.ml b/helm/gTopLevel/logicalOperations.ml
index 93c511f13..3fab938a0 100644
--- a/helm/gTopLevel/logicalOperations.ml
+++ b/helm/gTopLevel/logicalOperations.ml
@@ -94,8 +94,10 @@ let to_sequent id ids_to_terms ids_to_father_ids =
        None -> assert false
      | Some (_,metasenv,_,_) -> metasenv
    in
-    let ty = CicTypeChecker.type_of_aux' metasenv context term in
-     P.perforate context term ty (* P.perforate also sets the goal *)
+    let ty,_ = (* TASSI: FIXME ehhmmmm *)
+      CicTypeChecker.type_of_aux' metasenv context term CicUniv.empty_ugraph 
+    in
+      P.perforate context term ty (* P.perforate also sets the goal *)
 ;;
 
 exception FocusOnlyOnMeta;;
@@ -110,8 +112,10 @@ let focus id ids_to_terms ids_to_father_ids =
        None -> assert false
      | Some (_,metasenv,_,_) -> metasenv
    in
-    let ty = CicTypeChecker.type_of_aux' metasenv context term in
-     match term with
-        Cic.Meta (n,_) -> P.goal := Some n
-      | _ -> raise FocusOnlyOnMeta
+    let ty,_ = 
+      CicTypeChecker.type_of_aux' metasenv context term CicUniv.empty_ugraph 
+    in
+      match term with
+          Cic.Meta (n,_) -> P.goal := Some n
+	| _ -> raise FocusOnlyOnMeta
 ;;