From: Stefano Zacchiroli Date: Tue, 6 Apr 2004 12:08:23 +0000 (+0000) Subject: The parser accepts terms with metavariables as statements of theorems ==> X-Git-Tag: dead_dir_walking~80 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=c517601da65ba49769c401105d36c293a2c92a71;p=helm.git The parser accepts terms with metavariables as statements of theorems ==> metavariable instantiation must be propagated also on the theorem statement. --- diff --git a/helm/ocaml/tactics/proofEngineHelpers.ml b/helm/ocaml/tactics/proofEngineHelpers.ml index aec43abc3..2d576c3d8 100644 --- a/helm/ocaml/tactics/proofEngineHelpers.ml +++ b/helm/ocaml/tactics/proofEngineHelpers.ml @@ -48,7 +48,11 @@ let subst_meta_in_proof proof meta term newmetasenv = ) metasenv' in let bo' = subst_in bo in - let newproof = uri,metasenv'',bo',ty 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 *) @@ -66,6 +70,10 @@ let subst_meta_in_proof proof meta term 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 -> @@ -85,6 +93,6 @@ let subst_meta_and_metasenv_in_proof proof meta subst_in newmetasenv = | _ -> i ) newmetasenv [] in - let newproof = uri,metasenv',bo',ty in + let newproof = uri,metasenv',bo',ty' in (newproof, metasenv')