X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2FproofEngineReduction.ml;h=9e5aa04ff6c71142660110f2e1513c532d45f54f;hb=e7e2a523299d807370b292b44e77f46fad1638c9;hp=c70be1fb736b61b4da38d15c491f2e5d77579f18;hpb=bac72fcaa876137ab7a5630e0c1badc2a627dce8;p=helm.git

diff --git a/helm/ocaml/tactics/proofEngineReduction.ml b/helm/ocaml/tactics/proofEngineReduction.ml
index c70be1fb7..9e5aa04ff 100644
--- a/helm/ocaml/tactics/proofEngineReduction.ml
+++ b/helm/ocaml/tactics/proofEngineReduction.ml
@@ -382,7 +382,7 @@ let reduce context =
       C.Rel n as t ->
        (match List.nth context (n-1) with
            Some (_,C.Decl _) -> if l = [] then t else C.Appl (t::l)
-         | Some (_,C.Def bo) -> reduceaux context l (S.lift n bo)
+         | Some (_,C.Def (bo,_)) -> reduceaux context l (S.lift n bo)
 	 | None -> raise RelToHiddenHypothesis
        )
     | C.Var (uri,exp_named_subst) ->
@@ -604,7 +604,7 @@ let simpl context =
       C.Rel n as t ->
        (match List.nth context (n-1) with
            Some (_,C.Decl _) -> if l = [] then t else C.Appl (t::l)
-         | Some (_,C.Def bo) ->
+         | Some (_,C.Def (bo,_)) ->
             try_delta_expansion l t (S.lift n bo)
 	 | None -> raise RelToHiddenHypothesis
        )