diff options
| author | Matthieu Sozeau | 2014-06-11 17:19:14 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-06-11 17:19:14 +0200 |
| commit | a4db087565dd2ecfa3bcc022277bed1a3c868fd3 (patch) | |
| tree | d7479089105c6d0f4ba7d56721a98b95353d47cd /tactics/rewrite.ml | |
| parent | 99cdbc25a3a92545544a087ed55240c488b42fc9 (diff) | |
Fix bug #3291, stack overflow in rewrite.
Diffstat (limited to 'tactics/rewrite.ml')
| -rw-r--r-- | tactics/rewrite.ml | 3 |
1 files changed, 2 insertions, 1 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 *) |