X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FlogicalOperations.ml;h=93c511f138336469b9bb5b3e9cc046effc9dd69f;hb=c25a2152b1ebb7e9833db7c705e257068d89057a;hp=448c83a18fe925f0db84af9c2ded5cb45ebe8f15;hpb=c706b1cb2c7cbdd23a3281d35d3f0b10c3a684cf;p=helm.git

diff --git a/helm/gTopLevel/logicalOperations.ml b/helm/gTopLevel/logicalOperations.ml
index 448c83a18..93c511f13 100644
--- 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,7 +90,7 @@ 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
@@ -106,7 +106,7 @@ 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