1 (* Copyright (C) 2002, HELM Team.
3 * This file is part of HELM, an Hypertextual, Electronic
4 * Library of Mathematics, developed at the Computer Science
5 * Department, University of Bologna, Italy.
7 * HELM is free software; you can redistribute it and/or
8 * modify it under the terms of the GNU General Public License
9 * as published by the Free Software Foundation; either version 2
10 * of the License, or (at your option) any later version.
12 * HELM is distributed in the hope that it will be useful,
13 * but WITHOUT ANY WARRANTY; without even the implied warranty of
14 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
15 * GNU General Public License for more details.
17 * You should have received a copy of the GNU General Public License
18 * along with HELM; if not, write to the Free Software
19 * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
22 * For details, see the HELM World-Wide-Web page,
23 * http://cs.unibo.it/helm/.
28 let clearbody ~status:(proof, goal) ~hyp =
32 | Some (_, C.Decl _) -> raise (Fail "No Body To Clear")
33 | Some (n_to_clear_body, C.Def term) as hyp_to_clear_body ->
34 let curi,metasenv,pbo,pty =
37 | Some (curi,metasenv,bo,ty) -> curi,metasenv,bo,ty
42 | Some metano -> List.find (function (m,_,_) -> m=metano) metasenv
52 (m,canonical_context,ty) when m = metano ->
53 let canonical_context' =
57 t when t == hyp_to_clear_body ->
60 CicTypeChecker.type_of_aux' metasenv context term
62 Some (n_to_clear_body, Cic.Decl ty)
64 cleared_entry::context
65 | None -> None::context
70 CicTypeChecker.type_of_aux' metasenv context t
75 ("The correctness of hypothesis " ^
77 " relies on the body of " ^
78 string_of_name n_to_clear_body)
82 ) canonical_context []
86 CicTypeChecker.type_of_aux' metasenv canonical_context' ty
91 ("The correctness of the goal relies on the body of " ^
92 string_of_name n_to_clear_body))
94 m,canonical_context',ty
98 (Some (curi,metasenv',pbo,pty), goal)
100 let clear ~status:(proof, goal) ~hyp:hyp_to_clear =
101 let module C = Cic in
102 match hyp_to_clear with
104 | Some (n_to_clear, _) ->
105 let curi,metasenv,pbo,pty =
108 | Some (curi,metasenv,bo,ty) -> curi,metasenv,bo,ty
110 let metano,context,ty =
113 | Some metano -> List.find (function (m,_,_) -> m=metano) metasenv
123 (m,canonical_context,ty) when m = metano ->
124 let canonical_context' =
126 (fun entry context ->
128 t when t == hyp_to_clear -> None::context
129 | None -> None::context
131 | Some (n,C.Def t) ->
134 CicTypeChecker.type_of_aux' metasenv context t
141 " uses hypothesis " ^
142 string_of_name n_to_clear)
146 ) canonical_context []
150 CicTypeChecker.type_of_aux' metasenv canonical_context' ty
155 ("Hypothesis " ^ string_of_name n_to_clear ^
156 " occurs in the goal"))
158 m,canonical_context',ty
162 (Some (curi,metasenv',pbo,pty), goal)