From c517601da65ba49769c401105d36c293a2c92a71 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Tue, 6 Apr 2004 12:08:23 +0000 Subject: [PATCH] The parser accepts terms with metavariables as statements of theorems ==> metavariable instantiation must be propagated also on the theorem statement. --- helm/ocaml/tactics/proofEngineHelpers.ml | 12 ++++++++++-- 1 file changed, 10 insertions(+), 2 deletions(-) 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') -- 2.39.2