X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FlogicalOperations.ml;h=5d06c95d21b55a94c72178eba18d9198771d68db;hb=7cb90c67bc6f8113188a91ecc29f6db20db5aeb8;hp=9144f4740e1aa52e31b71c9c978e1ab0e269947c;hpb=76cb30ecd0159512548aee0ba7085ab17c6fd5bd;p=helm.git

diff --git a/helm/gTopLevel/logicalOperations.ml b/helm/gTopLevel/logicalOperations.ml
index 9144f4740..5d06c95d2 100644
--- a/helm/gTopLevel/logicalOperations.ml
+++ b/helm/gTopLevel/logicalOperations.ml
@@ -48,7 +48,7 @@ let get_context ids_to_terms ids_to_father_ids =
          | C.Prod _ -> []
          | C.Lambda (n,s,t) when t == term -> [Some (n,C.Decl s)]
          | C.Lambda _ -> []
-         | C.LetIn (n,s,t) when t == term -> [Some (n,C.Def s)]
+         | C.LetIn (n,s,t) when t == term -> [Some (n,C.Def (s,None))]
          | C.LetIn _ -> []
          | C.Appl _
          | C.Const _ -> []
@@ -60,7 +60,9 @@ let get_context ids_to_terms ids_to_father_ids =
             let counter = ref 0 in
              List.rev_map
               (function (name,_,ty,bo) ->
-                let res = Some (C.Name name, (C.Def (C.Fix (!counter,ifl)))) in
+                let res =
+                 Some (C.Name name, (C.Def ((C.Fix (!counter,ifl)), Some ty)))
+                in
                  incr counter ;
                  res
               ) ifl
@@ -68,7 +70,9 @@ let get_context ids_to_terms ids_to_father_ids =
             let counter = ref 0 in
              List.rev_map
               (function (name,ty,bo) ->
-                let res = Some (C.Name name,(C.Def (C.CoFix (!counter,ifl)))) in
+                let res =
+                 Some (C.Name name,(C.Def ((C.CoFix (!counter,ifl)), Some ty)))
+                in
                  incr counter ;
                  res
               ) ifl
@@ -86,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
@@ -102,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