Procedural: 2 bug fix in eta expansion + 1 bug fix in pattern generation

[helm.git] / components / tactics / proofEngineHelpers.ml

diff --git a/components/tactics/proofEngineHelpers.ml b/components/tactics/proofEngineHelpers.ml
index 9dfad7651cdc555abedf4ed1f71233ebce45059f..c2d0d15e171586b339f2fa32cd695cac1d063c54 100644 (file)
--- a/components/tactics/proofEngineHelpers.ml
+++ b/components/tactics/proofEngineHelpers.ml
@@ -27,11 +27,11 @@
 
 exception Bad_pattern of string Lazy.t
 
-let new_meta_of_proof ~proof:(_, metasenv, _, _) =
+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 uri,metasenv,bo,ty, attrs = proof in
    (* empty context is ok for term since it wont be used by apply_subst *)
    (* hack: since we do not know the context and the type of term, we
       create a substitution with cc =[] and type = Implicit; they will be
@@ -62,7 +62,7 @@ let subst_meta_in_proof proof meta term newmetasenv =
       * 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
+      let newproof = uri,metasenv'',bo',ty', attrs in
        (newproof, metasenv'')
 
 (*CSC: commento vecchio *)
@@ -78,7 +78,7 @@ let subst_meta_in_proof proof meta term newmetasenv =
 (*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 (uri,_,bo,ty, attrs) = 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
@@ -104,7 +104,7 @@ 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', attrs in
     (newproof, metasenv')
 
 let compare_metasenvs ~oldmetasenv ~newmetasenv =