+++ /dev/null
-(* 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 new_meta_of_proof ~proof:(_, metasenv, _, _) =
- CicMkImplicit.new_meta metasenv
-
-let subst_meta_in_proof proof meta term newmetasenv =
- let uri,metasenv,bo,ty = proof in
- let subst_in = CicMetaSubst.apply_subst [meta,term] in
- let metasenv' =
- newmetasenv @ (List.filter (function (m,_,_) -> m <> meta) metasenv)
- in
- let metasenv'' =
- List.map
- (function i,canonical_context,ty ->
- let canonical_context' =
- List.map
- (function
- Some (n,Cic.Decl s) -> Some (n,Cic.Decl (subst_in s))
- | Some (n,Cic.Def (s,None)) -> Some (n,Cic.Def ((subst_in s),None))
- | None -> None
- | Some (_,Cic.Def (_,Some _)) -> assert false
- ) canonical_context
- in
- i,canonical_context',(subst_in ty)
- ) metasenv'
- in
- let bo' = subst_in bo in
- (* Metavariables can appear also in the *statement* of the theorem
- * since the parser does not reject as statements terms with
- * metavariable therein *)
- let ty' = subst_in ty in
- let newproof = uri,metasenv'',bo',ty' in
- (newproof, metasenv'')
-
-(*CSC: commento vecchio *)
-(* refine_meta_with_brand_new_metasenv meta term subst_in newmetasenv *)
-(* This (heavy) function must be called when a tactic can instantiate old *)
-(* metavariables (i.e. existential variables). It substitues the metasenv *)
-(* of the proof with the result of removing [meta] from the domain of *)
-(* [newmetasenv]. Then it replaces Cic.Meta [meta] with [term] everywhere *)
-(* in the current proof. Finally it applies [apply_subst_replacing] to *)
-(* current proof. *)
-(*CSC: A questo punto perche' passare un bo' gia' istantiato, se tanto poi *)
-(*CSC: ci ripasso sopra apply_subst!!! *)
-(*CSC: Attenzione! Ora questa funzione applica anche [subst_in] a *)
-(*CSC: [newmetasenv]. *)
-let subst_meta_and_metasenv_in_proof proof meta subst_in newmetasenv =
- let (uri,_,bo,ty) = proof in
- let bo' = subst_in bo in
- (* Metavariables can appear also in the *statement* of the theorem
- * since the parser does not reject as statements terms with
- * metavariable therein *)
- let ty' = subst_in ty in
- let metasenv' =
- List.fold_right
- (fun metasenv_entry i ->
- match metasenv_entry with
- (m,canonical_context,ty) when m <> meta ->
- let canonical_context' =
- List.map
- (function
- None -> None
- | Some (i,Cic.Decl t) -> Some (i,Cic.Decl (subst_in t))
- | Some (i,Cic.Def (t,None)) ->
- Some (i,Cic.Def ((subst_in t),None))
- | Some (_,Cic.Def (_,Some _)) -> assert false
- ) canonical_context
- in
- (m,canonical_context',subst_in ty)::i
- | _ -> i
- ) newmetasenv []
- in
- let newproof = uri,metasenv',bo',ty' in
- (newproof, metasenv')
-