From e43abf43a78a5bbeed720d50cd1ea68fdfc672f2 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Fri, 27 Feb 2015 17:27:12 +0100
Subject: simpl: honor Global for "simpl: never" (Close: 3206)

It was an integer overflow!  All sorts of memories.
---
 pretyping/reductionops.ml | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 2c70a6c9a0..09eb38bd12 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -64,7 +64,10 @@ module ReductionBehaviour = struct
         if Lib.is_in_section (ConstRef c) then
           let vars, _, _ = Lib.section_segment_of_constant c in
           let extra = List.length vars in
-          let nargs' = if b.b_nargs < 0 then b.b_nargs else b.b_nargs + extra in
+          let nargs' =
+             if b.b_nargs = max_int then max_int
+             else if b.b_nargs < 0 then b.b_nargs
+             else b.b_nargs + extra in
           let recargs' = List.map ((+) extra) b.b_recargs in
           { b with b_nargs = nargs'; b_recargs = recargs' }
         else b
-- 
cgit v1.2.3