This commit was manufactured by cvs2svn to create branch 'init'.

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

diff --git a/helm/gTopLevel/proofEngineStructuralRules.ml b/helm/gTopLevel/proofEngineStructuralRules.ml
deleted file mode 100644 (file)
index e01f95e..0000000
--- a/helm/gTopLevel/proofEngineStructuralRules.ml
+++ /dev/null
@@ -1,149 +0,0 @@
-(* 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/.
- *)
-
-open ProofEngineTypes
-
-let clearbody ~hyp ~status:(proof, goal) =
- let module C = Cic in
-  match hyp with
-     None -> assert false
-   | Some (_, C.Decl _) -> raise (Fail "No Body To Clear")
-   | Some (n_to_clear_body, C.Def term) as hyp_to_clear_body ->
-      let curi,metasenv,pbo,pty = proof in
-       let metano,_,_ = List.find (function (m,_,_) -> m=goal) metasenv in
-        let string_of_name =
-         function
-            C.Name n -> n
-          | C.Anonimous -> "_"
-        in
-        let metasenv' =
-         List.map
-          (function
-              (m,canonical_context,ty) when m = metano ->
-                let canonical_context' =
-                 List.fold_right
-                  (fun entry context ->
-                    match entry with
-                       t when t == hyp_to_clear_body ->
-                        let cleared_entry =
-                         let ty =
-                          CicTypeChecker.type_of_aux' metasenv context term
-                         in
-                          Some (n_to_clear_body, Cic.Decl ty)
-                        in
-                         cleared_entry::context
-                     | None -> None::context
-                     | Some (n,C.Decl t)
-                     | Some (n,C.Def t) ->
-                        let _ =
-                         try
-                          CicTypeChecker.type_of_aux' metasenv context t
-                         with
-                          _ ->
-                            raise
-                             (Fail
-                               ("The correctness of hypothesis " ^
-                                string_of_name n ^
-                                " relies on the body of " ^
-                                string_of_name n_to_clear_body)
-                             )
-                        in
-                         entry::context
-                  ) canonical_context []
-                in
-                 let _ =
-                  try
-                   CicTypeChecker.type_of_aux' metasenv canonical_context' ty
-                  with
-                   _ ->
-                    raise
-                     (Fail
-                      ("The correctness of the goal relies on the body of " ^
-                       string_of_name n_to_clear_body))
-                 in
-                  m,canonical_context',ty
-            | t -> t
-          ) metasenv
-        in
-         (curi,metasenv',pbo,pty), [goal]
-
-let clear ~hyp:hyp_to_clear ~status:(proof, goal) =
- let module C = Cic in
-  match hyp_to_clear with
-     None -> assert false
-   | Some (n_to_clear, _) ->
-      let curi,metasenv,pbo,pty = proof in
-       let metano,context,ty =
-        List.find (function (m,_,_) -> m=goal) metasenv
-       in
-        let string_of_name =
-         function
-            C.Name n -> n
-          | C.Anonimous -> "_"
-        in
-        let metasenv' =
-         List.map
-          (function
-              (m,canonical_context,ty) when m = metano ->
-                let canonical_context' =
-                 List.fold_right
-                  (fun entry context ->
-                    match entry with
-                       t when t == hyp_to_clear -> None::context
-                     | None -> None::context
-                     | Some (n,C.Decl t)
-                     | Some (n,C.Def t) ->
-                        let _ =
-                         try
-                          CicTypeChecker.type_of_aux' metasenv context t
-                         with
-                          _ ->
-                            raise
-                             (Fail
-                               ("Hypothesis " ^
-                                string_of_name n ^
-                                " uses hypothesis " ^
-                                string_of_name n_to_clear)
-                             )
-                        in
-                         entry::context
-                  ) canonical_context []
-                in
-                 let _ =
-                  try
-                   CicTypeChecker.type_of_aux' metasenv canonical_context' ty
-                  with
-                   _ ->
-                    raise
-                     (Fail
-                      ("Hypothesis " ^ string_of_name n_to_clear ^
-                       " occurs in the goal"))
-                 in
-                  m,canonical_context',ty
-            | t -> t
-          ) metasenv
-        in
-         (curi,metasenv',pbo,pty), [goal]
-