Incredible bug of simpl fixed: the stack (in the terminology used for the

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

diff --git a/helm/ocaml/tactics/proofEngineReduction.ml b/helm/ocaml/tactics/proofEngineReduction.ml
index af41d8ee8b42508e0ec802e7b705fdc13edf9a0b..8a6ef81a277658d5e7cda8055768a925b7b3e574 100644 (file)
--- a/helm/ocaml/tactics/proofEngineReduction.ml
+++ b/helm/ocaml/tactics/proofEngineReduction.ml
@@ -596,6 +596,7 @@ exception AlreadySimplified;;
 (*     change in every iteration, i.e. to the actual arguments for the       *)
 (*     lambda-abstractions that precede the Fix.                             *)
 (*CSC: It does not perform simplification in a Case *)
+
 let simpl context =
  (* reduceaux is equal to the reduceaux locally defined inside *)
  (* reduce, but for the const case.                            *) 
@@ -605,12 +606,14 @@ let simpl context =
   let module S = CicSubstitution in
    function
       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,_)) ->
-            try_delta_expansion l t (S.lift n bo)
-        | None -> raise RelToHiddenHypothesis
-       )
+       (try
+         match List.nth context (n-1) with
+            Some (_,C.Decl _) -> if l = [] then t else C.Appl (t::l)
+          | Some (_,C.Def (bo,_)) ->
+             try_delta_expansion context l t (S.lift n bo)
+         | None -> raise RelToHiddenHypothesis
+        with
+         Failure _ -> assert false)
     | C.Var (uri,exp_named_subst) ->
        let exp_named_subst' =
         reduceaux_exp_named_subst context l exp_named_subst
@@ -659,7 +662,7 @@ let simpl context =
         (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
          match o with
            C.Constant (_,Some body,_,_,_) ->
-            try_delta_expansion l
+            try_delta_expansion context l
              (C.Const (uri,exp_named_subst'))
              (CicSubstitution.subst_vars exp_named_subst' body)
          | C.Constant (_,None,_,_,_) ->
@@ -798,7 +801,7 @@ let simpl context =
  and reduceaux_exp_named_subst context l =
   List.map (function uri,t -> uri,reduceaux context [] t)
  (**** Step 2 ****)
- and try_delta_expansion l term body =
+ and try_delta_expansion context l term body =
   let module C = Cic in
   let module S = CicSubstitution in
    try