X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2FreductionTactics.ml;h=754b2c0c5b49cca403f94a8e3bde1ee86f2c9798;hb=3f676ab6acafa32514a44bc84d287f44dbc5389e;hp=115faa80b65a58c88256f0f7cb8d05e8d903002d;hpb=55b82bd235d82ff7f0a40d980effe1efde1f5073;p=helm.git

diff --git a/helm/software/components/tactics/reductionTactics.ml b/helm/software/components/tactics/reductionTactics.ml
index 115faa80b..754b2c0c5 100644
--- a/helm/software/components/tactics/reductionTactics.ml
+++ b/helm/software/components/tactics/reductionTactics.ml
@@ -30,7 +30,7 @@ open ProofEngineTypes
 (* Note: this code is almost identical to change_tac and
 *  it could be unified by making the change function a callback *)
 let reduction_tac ~reduction ~pattern (proof,goal) =
-  let curi,metasenv,pbo,pty = proof in
+  let curi,metasenv,pbo,pty, attrs = proof in
   let (metano,context,ty) as conjecture = CicUtil.lookup_meta goal metasenv in
   let change subst where terms metasenv ugraph =
    if terms = [] then where, metasenv, ugraph
@@ -88,7 +88,7 @@ let reduction_tac ~reduction ~pattern (proof,goal) =
       | _ as t -> t
     ) metasenv
   in
-  (curi,metasenv',pbo,pty), [metano]
+  (curi,metasenv',pbo,pty, attrs), [metano]
 ;;
 
 let simpl_tac ~pattern =
@@ -131,7 +131,7 @@ exception NotConvertible
         term(s) to be replaced. *)
 let change_tac ~pattern with_what  =
  let change_tac ~pattern ~with_what (proof, goal) =
-  let curi,metasenv,pbo,pty = proof in
+  let curi,metasenv,pbo,pty, attrs = proof in
   let (metano,context,ty) as conjecture = CicUtil.lookup_meta goal metasenv in
   let change subst where terms metasenv ugraph =
    if terms = [] then where, metasenv, ugraph
@@ -200,7 +200,7 @@ let change_tac ~pattern with_what  =
         | _ as t -> t)
       metasenv
   in
-  (curi,metasenv',pbo,pty), [metano]
+  (curi,metasenv',pbo,pty, attrs), [metano]
   in
     mk_tactic (change_tac ~pattern ~with_what)