From: Stefano Zacchiroli <zack@upsilon.cc>
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')