From 83608720aac2a0a464649aca8b2a23ce395679ae Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 7 Apr 2016 14:58:27 +0200
Subject: Fixing an incorrect use of prod_appvect on a term which was not a
 product in setoid_rewrite.

Backport of d670c6b6ce from trunk.
---
 tactics/rewrite.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml
index 803e187ff5..21abafbf18 100644
--- a/tactics/rewrite.ml
+++ b/tactics/rewrite.ml
@@ -1028,7 +1028,7 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy =
 		      | x -> x
 		    in
 		    let res =
-		      { rew_car = prod_appvect r.rew_car args;
+		      { rew_car = Reductionops.hnf_prod_appvect env (goalevars evars) r.rew_car args;
 			rew_from = mkApp(r.rew_from, args); rew_to = mkApp(r.rew_to, args);
 			rew_prf = prf; rew_evars = r.rew_evars }
 		    in 
-- 
cgit v1.2.3