Fix bug #3291, stack overflow in rewrite.

2 files changed, 31 insertions, 2 deletions

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