Defs in context may now have an optional type (when unknown).

[helm.git] / helm / ocaml / tactics / proofEngineReduction.ml

diff --git a/helm/ocaml/tactics/proofEngineReduction.ml b/helm/ocaml/tactics/proofEngineReduction.ml
index c70be1fb736b61b4da38d15c491f2e5d77579f18..9e5aa04ff6c71142660110f2e1513c532d45f54f 100644 (file)
--- 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
        )