diff options
| author | Enrico Tassi | 2015-02-27 17:27:12 +0100 |
|---|---|---|
| committer | Enrico Tassi | 2015-02-27 17:27:12 +0100 |
| commit | e43abf43a78a5bbeed720d50cd1ea68fdfc672f2 (patch) | |
| tree | 5b8a1fe63be6c18be199faf05902e4c465247e67 | |
| parent | eb3e8efaaafd0de673184db85b9b647cfa24dd92 (diff) | |
simpl: honor Global for "simpl: never" (Close: 3206)
It was an integer overflow! All sorts of memories.
| -rw-r--r-- | pretyping/reductionops.ml | 5 |
1 files changed, 4 insertions, 1 deletions
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 |