This commit was manufactured by cvs2svn to create branch

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

diff --git a/helm/gTopLevel/logicalOperations.ml b/helm/gTopLevel/logicalOperations.ml
deleted file mode 100644 (file)
index a9274fb..0000000
--- a/helm/gTopLevel/logicalOperations.ml
+++ /dev/null
@@ -1,89 +0,0 @@
-let get_parent id ids_to_terms ids_to_father_ids =
- match Hashtbl.find ids_to_father_ids id with
-    None -> None
-  | Some id -> Some (id, Hashtbl.find ids_to_terms id)
-;;
-
-let get_context ids_to_terms ids_to_father_ids =
- let module C = Cic in
-  let rec aux id =
-   match get_parent id ids_to_terms ids_to_father_ids with
-      None -> []
-    | Some (parentid,parent) ->
-       let term = Hashtbl.find ids_to_terms id in
-       let binding =
-        match parent with
-           C.Rel _
-         | C.Var _
-         | C.Meta _
-         | C.Sort _
-         | 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 _ -> []
-         | C.Appl _
-         | C.Const _ -> []
-         | C.Abst _ -> assert false
-         | C.MutInd _
-         | C.MutConstruct _
-         | C.MutCase _ -> []
-(*CSC: sbagliato: manca il when *)
-         | C.Fix (_,ifl) ->
-            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
-                 incr counter ;
-                 res
-              ) ifl
-         | C.CoFix (_,ifl) ->
-            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
-                 incr counter ;
-                 res
-              ) ifl
-       in
-        binding@(aux parentid)
-  in
-   aux
-;;
-
-exception NotImplemented;;
-
-(* A subterm is changed into a fresh meta *)
-let to_sequent id ids_to_terms ids_to_father_ids =
- let module P = ProofEngine in
-  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
-       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 *)
-;;
-
-exception FocusOnlyOnMeta;;
-
-(* If the current selection is a Meta, that Meta becomes the current goal *)
-let focus id ids_to_terms ids_to_father_ids =
- let module P = ProofEngine in
-  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
-       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
-;;