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

Krivine's machine) was processed in the wrong context. As a result List.nth
(to get a Rel in the context) used to raise Failure in several cases. The
Failure, however, was catched somewhere in the code of matita and the
failure of simpl was hidden in most of the cases.

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