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

diff --git a/helm/gTopLevel/logicalOperations.ml b/helm/gTopLevel/logicalOperations.ml
index a9274fba6..93c511f13 100644
--- a/helm/gTopLevel/logicalOperations.ml
+++ b/helm/gTopLevel/logicalOperations.ml
@@ -1,3 +1,28 @@
+(* Copyright (C) 2002, HELM Team.
+ * 
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ * 
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ * 
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA  02111-1307, USA.
+ * 
+ * For details, see the HELM World-Wide-Web page,
+ * http://cs.unibo.it/helm/.
+ *)
+
 let get_parent id ids_to_terms ids_to_father_ids =
  match Hashtbl.find ids_to_father_ids id with
     None -> None
@@ -17,17 +42,16 @@ 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 _ -> []
          | 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 _ -> []
-         | C.Abst _ -> assert false
          | C.MutInd _
          | C.MutConstruct _
          | C.MutCase _ -> []
@@ -36,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
@@ -44,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
@@ -62,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
@@ -78,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