From d7a9fea94772971a52d04f9f266fe6d5e25cd40e Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Mon, 2 May 2016 15:42:10 +0200
Subject: Avoid infinite loop/stack overflow when using "simpl nomatch" (bug
 #4576).

When encountering a "simpl nomatch" constant, the reduction machinery tries
to unfold it. If the subsequent partial reduction does not produce any
match construct, it keeps going from the reduced term. Unfortunately, the
reduced term has been refolded in the meantime, which means that some of
the previous reduction steps have been canceled, thus causing an infinite
loop. This patch delays the refolding till the very end, so that reduction
always progresses.

Disclaimer: I have no idea what I am doing here. The patch compiles the
standard library and the test suite properly, so hopefully they contain
enough tests to exercise the reduction machinery.
---
 pretyping/reductionops.ml | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

(limited to 'pretyping')

diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 13b7fb4079..7c7b31395e 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -811,7 +811,7 @@ let rec whd_state_gen ?csts tactic_mode flags env sigma =
     let fold () =
       let () = if !debug_RAKAM then
 	  let open Pp in pp (str "<><><><><>" ++ fnl ()) in
-      if tactic_mode then (Stack.best_state s cst_l,Cst_stack.empty) else (s,cst_l)
+      (s,cst_l)
     in
     match kind_of_term x with
     | Rel n when Closure.RedFlags.red_set flags Closure.RedFlags.fDELTA ->
@@ -1002,7 +1002,9 @@ let rec whd_state_gen ?csts tactic_mode flags env sigma =
     | Rel _ | Var _ | Const _ | LetIn _ | Proj _ -> fold ()
     | Sort _ | Ind _ | Prod _ -> fold ()
   in
-  whrec (Option.default Cst_stack.empty csts)
+  fun xs ->
+  let (s,cst_l as res) = whrec (Option.default Cst_stack.empty csts) xs in
+  if tactic_mode then (Stack.best_state s cst_l,Cst_stack.empty) else res
 
 (** reduction machine without global env and refold machinery *)
 let local_whd_state_gen flags sigma =
-- 
cgit v1.2.3


From 443857fe1bbecf089eb40d522a71a014273c5a23 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Tue, 3 May 2016 14:06:17 +0200
Subject: Use the canonical name when looking for an eliminator (bug #4670).

Disclaimer: I have no idea what I am doing.
---
 pretyping/indrec.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'pretyping')

diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml
index 0588dcc87f..589b8d82ab 100644
--- a/pretyping/indrec.ml
+++ b/pretyping/indrec.ml
@@ -598,7 +598,7 @@ let make_elimination_ident id s = add_suffix id (elimination_suffix s)
 
 let lookup_eliminator ind_sp s =
   let kn,i = ind_sp in
-  let mp,dp,l = repr_mind kn in
+  let mp,dp,l = KerName.repr (MutInd.canonical kn) in
   let ind_id = (Global.lookup_mind kn).mind_packets.(i).mind_typename in
   let id = add_suffix ind_id (elimination_suffix s) in
   (* Try first to get an eliminator defined in the same section as the *)
-- 
cgit v1.2.3