From 4ed609a7351882664acd5b5f1525700e7150ce0e Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 15 Feb 2015 13:57:45 +0100
Subject: Fixing bug #3916.

---
 pretyping/tacred.ml | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 1106fefa39..9d6eb31b44 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -1211,9 +1211,10 @@ let one_step_reduce env sigma c =
 	       (ci,p,c,lf), stack)
            with Redelimination -> raise NotStepReducible)
       | Fix fix ->
-	  (match reduce_fix (whd_construct_stack env) sigma fix stack with
+	  (try match reduce_fix (whd_construct_stack env) sigma fix stack with
              | Reduced s' -> s'
-	     | NotReducible -> raise NotStepReducible)
+	     | NotReducible -> raise NotStepReducible
+           with Redelimination -> raise NotStepReducible)
       | _ when isEvalRef env x ->
 	  let ref,u = destEvalRefU x in
           (try
-- 
cgit v1.2.3