From c1e1e52311745ac5bad85b49d76c8ff327d6e74f Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 16 Oct 2014 13:04:47 +0200
Subject: Fixing decompose_app_rel in Rewrite.

The old implementation did not beta-iota normalize before observing the head of
the term, resulting in stange bugs.
---
 tactics/rewrite.ml | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml
index 6891f94371..69bceb0d34 100644
--- a/tactics/rewrite.ml
+++ b/tactics/rewrite.ml
@@ -469,6 +469,8 @@ let get_symmetric_proof b =
   if b then PropGlobal.get_symmetric_proof else TypeGlobal.get_symmetric_proof
 
 let rec decompose_app_rel env evd t = 
+  (** Head normalize for compatibility with the old meta mechanism *)
+  let t = Reductionops.whd_betaiota evd t in
   match kind_of_term t with
   | App (f, args) -> 
       if Array.length args > 1 then 
-- 
cgit v1.2.3