Remove dead code in lazy reduction machine.

1 files changed, 6 insertions, 11 deletions

diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 3253cddf7c..2cf3f88735 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -56,8 +56,7 @@ let compare_stack_shape stk1 stk2 =
     | (_, Zapp l2::s2) -> compare_rec (bal-Array.length l2) stk1 s2
     | (Zproj (n1,m1,p1)::s1, Zproj (n2,m2,p2)::s2) ->
         Int.equal bal 0 && compare_rec 0 s1 s2
-    | ((Zcase(c1,_,_)|ZcaseT(c1,_,_,_))::s1,
-       (Zcase(c2,_,_)|ZcaseT(c2,_,_,_))::s2) ->
+    | (ZcaseT(c1,_,_,_)::s1, ZcaseT(c2,_,_,_)::s2) ->
         Int.equal bal 0 (* && c1.ci_ind  = c2.ci_ind *) && compare_rec 0 s1 s2
     | (Zfix(_,a1)::s1, Zfix(_,a2)::s2) ->
         Int.equal bal 0 && compare_rec 0 a1 a2 && compare_rec 0 s1 s2
@@ -91,9 +90,8 @@ let pure_stack lfts stk =
                 let (lfx,pa) = pure_rec l a in
                 (l, Zlfix((lfx,fx),pa)::pstk)
             | (ZcaseT(ci,p,br,e),(l,pstk)) ->
-                (l,Zlcase(ci,l,mk_clos e p,Array.map (mk_clos e) br)::pstk)
-            | (Zcase(ci,p,br),(l,pstk)) ->
-                (l,Zlcase(ci,l,p,br)::pstk)) in
+                (l,Zlcase(ci,l,mk_clos e p,Array.map (mk_clos e) br)::pstk))
+  in
   snd (pure_rec lfts stk)
 
 (****************************************************************************)
@@ -237,7 +235,6 @@ let rec no_arg_available = function
   | Zshift _ :: stk -> no_arg_available stk
   | Zapp v :: stk -> Int.equal (Array.length v) 0 && no_arg_available stk
   | Zproj _ :: _ -> true
-  | Zcase _ :: _ -> true
   | ZcaseT _ :: _ -> true
   | Zfix _ :: _ -> true
 
@@ -250,7 +247,6 @@ let rec no_nth_arg_available n = function
       if n >= k then no_nth_arg_available (n-k) stk
       else false
   | Zproj _ :: _ -> true
-  | Zcase _ :: _ -> true
   | ZcaseT _ :: _ -> true
   | Zfix _ :: _ -> true
 
@@ -260,13 +256,12 @@ let rec no_case_available = function
   | Zshift _ :: stk -> no_case_available stk
   | Zapp _ :: stk -> no_case_available stk
   | Zproj (_,_,p) :: _ -> false
-  | Zcase _ :: _ -> false
   | ZcaseT _ :: _ -> false
   | Zfix _ :: _ -> true
 
 let in_whnf (t,stk) =
   match fterm_of t with
-    | (FLetIn _ | FCase _ | FCaseT _ | FApp _ 
+    | (FLetIn _ | FCaseT _ | FApp _ 
 	  | FCLOS _ | FLIFT _ | FCast _) -> false
     | FLambda _ -> no_arg_available stk
     | FConstruct _ -> no_case_available stk
@@ -532,8 +527,8 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
         else raise NotConvertible
 
      (* Should not happen because both (hd1,v1) and (hd2,v2) are in whnf *)
-     | ( (FLetIn _, _) | (FCase _,_) | (FCaseT _,_) | (FApp _,_) | (FCLOS _,_) | (FLIFT _,_)
-       | (_, FLetIn _) | (_,FCase _) | (_,FCaseT _) | (_,FApp _) | (_,FCLOS _) | (_,FLIFT _)
+     | ( (FLetIn _, _) | (FCaseT _,_) | (FApp _,_) | (FCLOS _,_) | (FLIFT _,_)
+       | (_, FLetIn _) | (_,FCaseT _) | (_,FApp _) | (_,FCLOS _) | (_,FLIFT _)
        | (FLOCKED,_) | (_,FLOCKED) ) -> assert false
 
      (* In all other cases, terms are not convertible *)