From b286c9f4f42febfd37f9715d81eaf118ab24aa94 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 27 Feb 2015 16:29:28 +0100
Subject: Add support so that the type of a match in an inductive type with
 let-in is reduced as if without let-in, when applied to arguments.

This allows e.g. to have a head-betazeta-reduced goal in the following example.

Inductive Foo : let X := Set in X := I : Foo.
Definition foo (x : Foo) : x = x. destruct x. (* or case x, etc. *)
---
 pretyping/reductionops.ml | 13 +++++++++++++
 1 file changed, 13 insertions(+)

(limited to 'pretyping/reductionops.ml')

diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index ec34383820..2c70a6c9a0 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -1628,3 +1628,16 @@ let head_unfold_under_prod ts env _ c =
 	    | Const cst -> beta_applist (unfold cst,l)
 	    | _ -> c in
   aux c
+
+let betazetaevar_applist sigma n c l =
+  let rec stacklam n env t stack =
+    if Int.equal n 0 then applist (substl env t, stack) else
+    match kind_of_term t, stack with
+    | Lambda(_,_,c), arg::stacktl -> stacklam (n-1) (arg::env) c stacktl
+    | LetIn(_,b,_,c), _ -> stacklam (n-1) (b::env) c stack
+    | Evar ev, _ ->
+      (match safe_evar_value sigma ev with
+      | Some body -> stacklam n env body stack
+      | None -> applist (substl env t, stack))
+    | _ -> anomaly (Pp.str "Not enough lambda/let's") in
+  stacklam n [] c l
-- 
cgit v1.2.3


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(-)

(limited to 'pretyping/reductionops.ml')

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