From a4db087565dd2ecfa3bcc022277bed1a3c868fd3 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Wed, 11 Jun 2014 17:19:14 +0200
Subject: Fix bug #3291, stack overflow in rewrite.

---
 tactics/rewrite.ml            |  3 ++-
 tactics/rewrite.mli           | 30 +++++++++++++++++++++++++++++-
 test-suite/bugs/closed/3291.v |  9 +++++++++
 test-suite/bugs/opened/3291.v |  8 --------
 4 files changed, 40 insertions(+), 10 deletions(-)
 create mode 100644 test-suite/bugs/closed/3291.v
 delete mode 100644 test-suite/bugs/opened/3291.v

diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml
index aa0152d35a..7309e22759 100644
--- a/tactics/rewrite.ml
+++ b/tactics/rewrite.ml
@@ -295,7 +295,8 @@ end) = struct
     let ap = is_Prop ta and bp = is_Prop tb in
       if ap && bp then app_poly env evd impl [| a; b |], unfold_impl
       else if ap then (* Domain in Prop, CoDomain in Type *)
-	(evd, mkProd (Anonymous, a, b)), (fun x -> x)
+	(app_poly env evd arrow [| a; b |]), unfold_impl
+	(* (evd, mkProd (Anonymous, a, b)), (fun x -> x) *)
       else if bp then (* Dummy forall *)
 	(app_poly env evd coq_all [| a; mkLambda (Anonymous, a, b) |]), unfold_forall
       else (* None in Prop, use arrow *)
diff --git a/tactics/rewrite.mli b/tactics/rewrite.mli
index 0f155c8bb8..81f1175c4c 100644
--- a/tactics/rewrite.mli
+++ b/tactics/rewrite.mli
@@ -28,7 +28,24 @@ type ('constr,'redexpr) strategy_ast =
   | StratEval of 'redexpr 
   | StratFold of 'constr
 
-type strategy
+type rewrite_proof = 
+  | RewPrf of constr * constr
+  | RewCast of cast_kind
+
+type evars = evar_map * Evar.Set.t (* goal evars, constraint evars *)
+
+type rewrite_result_info = {
+  rew_car : constr;
+  rew_from : constr;
+  rew_to : constr;
+  rew_prf : rewrite_proof;
+  rew_evars : evars;
+}
+
+type rewrite_result = rewrite_result_info option
+
+type strategy = Environ.env -> Id.t list -> constr -> types ->
+  (bool (* prop *) * constr option) -> evars -> rewrite_result option
 
 val strategy_of_ast : (glob_constr_and_expr, raw_red_expr) strategy_ast -> strategy
 
@@ -78,3 +95,14 @@ val setoid_symmetry_in : Id.t -> unit Proofview.tactic
 val setoid_reflexivity : unit Proofview.tactic
 
 val setoid_transitivity : constr option -> unit Proofview.tactic
+
+
+val apply_strategy :
+  strategy ->
+  Environ.env ->
+  Names.Id.t list ->
+  Term.constr ->
+  bool * Term.constr ->
+  evars ->
+  (rewrite_proof * evars * Term.constr * Term.constr * Term.constr)
+    option option
diff --git a/test-suite/bugs/closed/3291.v b/test-suite/bugs/closed/3291.v
new file mode 100644
index 0000000000..4ea748c0fb
--- /dev/null
+++ b/test-suite/bugs/closed/3291.v
@@ -0,0 +1,9 @@
+Require Import Setoid.
+
+Definition segv : forall x, (x = 0%nat) -> (forall (y : nat), (y < x)%nat -> nat) = forall (y : nat), (y < 0)%nat -> nat.
+intros x eq.
+assert (H : forall y, (y < x)%nat = (y < 0)%nat).
+rewrite -> eq. auto.
+Set Typeclasses Debug.
+Fail setoid_rewrite <- H. (* The command has indeed failed with message:
+=> Stack overflow. *)
diff --git a/test-suite/bugs/opened/3291.v b/test-suite/bugs/opened/3291.v
deleted file mode 100644
index 4e1c2630e3..0000000000
--- a/test-suite/bugs/opened/3291.v
+++ /dev/null
@@ -1,8 +0,0 @@
-Require Import Setoid.
-
-Definition segv : forall x, (x = 0%nat) -> (forall (y : nat), (y < x)%nat -> nat) = forall (y : nat), (y < 0)%nat -> nat.
-intros x eq.
-assert (H : forall y, (y < x)%nat = (y < 0)%nat).
-rewrite -> eq. auto.
-Fail Timeout 1 setoid_rewrite <- H. (* The command has indeed failed with message:
-=> Stack overflow. *)
-- 
cgit v1.2.3