From 6ef9cd21b41fe34e4803778a783f47c84c9e04aa Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 7 Sep 2001 14:57:04 +0000
Subject: Extension à Cases et Fix de la réduction pas à pas vers un produit
 (Red)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1928 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/reduction.ml | 12 +++++-------
 1 file changed, 5 insertions(+), 7 deletions(-)

(limited to 'kernel')

diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 4832cdd8a4..5c0a4fa634 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -219,13 +219,11 @@ let contract_fix ((recindices,bodynum),(types,names,bodies as typedbodies)) =
   substl (list_tabulate make_Fi nbodies) bodies.(bodynum)
 
 let fix_recarg ((recindices,bodynum),_) stack =
-  if 0 <= bodynum & bodynum < Array.length recindices then
-    let recargnum = Array.get recindices bodynum in
-    (try 
-       Some (recargnum, stack_nth stack recargnum)
-     with Not_found ->
-       None)
-  else 
+  assert (0 <= bodynum & bodynum < Array.length recindices);
+  let recargnum = Array.get recindices bodynum in
+  try 
+    Some (recargnum, stack_nth stack recargnum)
+  with Not_found ->
     None
 
 type fix_reduction_result = NotReducible | Reduced of state
-- 
cgit v1.2.3