X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Ftactics%2FproofEngineStructuralRules.ml;h=ea7586e164f77c3a03079bdc9142481eb396ac70;hb=6e01bb1ae52fe45ce77a7f950efb5feb295e82b1;hp=636ea07c0f3c67d36ba04ae3dc4057a6de4b14e5;hpb=cd91767a396b7bbc72e6e3ee90a3b758421f935d;p=helm.git

diff --git a/components/tactics/proofEngineStructuralRules.ml b/components/tactics/proofEngineStructuralRules.ml
index 636ea07c0..ea7586e16 100644
--- a/components/tactics/proofEngineStructuralRules.ml
+++ b/components/tactics/proofEngineStructuralRules.ml
@@ -30,7 +30,7 @@ module C = Cic
 
 let clearbody ~hyp = 
  let clearbody (proof, goal) =
-   let curi,metasenv,pbo,pty, attrs = proof in
+   let curi,metasenv,_subst,pbo,pty, attrs = proof in
     let metano,_,_ = CicUtil.lookup_meta goal metasenv in
      let string_of_name =
       function
@@ -93,13 +93,13 @@ let clearbody ~hyp =
          | t -> t
        ) metasenv
      in
-      (curi,metasenv',pbo,pty, attrs), [goal]
+      (curi,metasenv',_subst,pbo,pty, attrs), [goal]
  in
   PET.mk_tactic clearbody
 
 let clear_one ~hyp =
  let clear_one (proof, goal) =
-   let curi,metasenv,pbo,pty, attrs = proof in
+   let curi,metasenv,_subst,pbo,pty, attrs = proof in
     let metano,context,ty =
      CicUtil.lookup_meta goal metasenv
     in
@@ -151,7 +151,7 @@ let clear_one ~hyp =
          | t -> t
        ) metasenv
      in
-      (curi,metasenv',pbo,pty, attrs), [goal]
+      (curi,metasenv',_subst,pbo,pty, attrs), [goal]
  in
   PET.mk_tactic clear_one
 
@@ -176,7 +176,7 @@ let rename ~froms ~tos =
          try List.combine froms tos
 	 with Invalid_argument _ -> raise (PET.Fail (lazy error))
       in
-      let curi, metasenv, pbo, pty, attrs = proof in
+      let curi, metasenv, _subst, pbo, pty, attrs = proof in
       let metano, _, _ = CicUtil.lookup_meta goal metasenv in      
       let rename_map = function
          | Some (Cic.Name hyp, decl_or_def) as entry ->
@@ -191,6 +191,6 @@ let rename ~froms ~tos =
          | conjecture -> conjecture
       in
       let metasenv = List.map map metasenv in
-      (curi, metasenv, pbo, pty, attrs), [goal]
+      (curi, metasenv, _subst, pbo, pty, attrs), [goal]
    in
    PET.mk_tactic rename