ocaml 3.09 transition

[helm.git] / helm / gTopLevel / logicalOperations.ml

diff --git a/helm/gTopLevel/logicalOperations.ml b/helm/gTopLevel/logicalOperations.ml
index 448c83a18fe925f0db84af9c2ded5cb45ebe8f15..3fab938a058360d73f93c9d9dcf4ec6b2892af72 100644 (file)
--- a/helm/gTopLevel/logicalOperations.ml
+++ b/helm/gTopLevel/logicalOperations.ml
@@ -42,7 +42,7 @@ let get_context ids_to_terms ids_to_father_ids =
          | C.Var _
          | C.Meta _
          | C.Sort _
-         | C.Implicit
+         | C.Implicit _
          | C.Cast _ -> []
          | C.Prod (n,s,t) when t == term -> [Some (n,C.Decl s)]
          | C.Prod _ -> []
@@ -90,12 +90,14 @@ let to_sequent id ids_to_terms ids_to_father_ids =
   let term = Hashtbl.find ids_to_terms id in
   let context = get_context ids_to_terms ids_to_father_ids id in
    let metasenv =
-    match !P.proof with
+    match P.get_proof () with
        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;;
@@ -106,12 +108,14 @@ let focus id ids_to_terms ids_to_father_ids =
   let term = Hashtbl.find ids_to_terms id in
   let context = get_context ids_to_terms ids_to_father_ids id in
    let metasenv =
-    match !P.proof with
+    match P.get_proof () with
        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
 ;;