X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2FreductionTactics.ml;h=55eacc234c3da15ffb057255dc73cf30391407f1;hb=265cf771fbfe217b5f274b999fc3ad887683a09a;hp=b29873a1fceae31c4521c231bfd503ce29b65585;hpb=edf601b6b8eb5b28a5292d0660a3b54b5680e580;p=helm.git

diff --git a/helm/ocaml/tactics/reductionTactics.ml b/helm/ocaml/tactics/reductionTactics.ml
index b29873a1f..55eacc234 100644
--- a/helm/ocaml/tactics/reductionTactics.ml
+++ b/helm/ocaml/tactics/reductionTactics.ml
@@ -69,11 +69,12 @@ let reduction_tac ~also_in_hypotheses ~reduction ~terms ~status:(proof,goal) =
       List.fold_right
        (fun entry context ->
          match entry with
-            Some (name,Cic.Def  t) ->
-             (Some (name,Cic.Def  (replace context t)))::context
+            Some (name,Cic.Def (t,None)) ->
+             (Some (name,Cic.Def ((replace context t),None)))::context
           | Some (name,Cic.Decl t) ->
              (Some (name,Cic.Decl (replace context t)))::context
           | None -> None::context
+          | Some (_,Cic.Def (_,Some _)) -> assert false
        ) context []
      else
       context
@@ -110,8 +111,9 @@ let fold_tac ~reduction ~also_in_hypotheses ~term ~status:(proof,goal) =
        List.map
         (function
             Some (n,Cic.Decl t) -> Some (n,Cic.Decl (replace t))
-          | Some (n,Cic.Def t)  -> Some (n,Cic.Def  (replace t))
+          | Some (n,Cic.Def (t,None))  -> Some (n,Cic.Def ((replace t),None))
           | None -> None
+          | Some (_,Cic.Def (_,Some _)) -> assert false
         ) context
       else
        context