From d223f85d0fd57ce74dcdcc8690a36f1ef87b408d Mon Sep 17 00:00:00 2001
From: herbelin
Date: Thu, 21 Mar 2013 19:13:04 +0000
Subject: Using hnf instead of "intro H" for forcing reduction to a product.
 Added full betaiota in hnf. This seems more natural, even if it changes the
 strict meaning of hnf. This is source of incompatibilities as "intro" might
 succeed more often.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16338 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 pretyping/tacred.ml | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

(limited to 'pretyping')

diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 86195edd22..508569f0d7 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -812,7 +812,7 @@ let try_red_product env sigma c =
 
 let red_product env sigma c =
   try try_red_product env sigma c
-  with Redelimination -> error "Not reducible."
+  with Redelimination -> error "No head constant to reduce."
 
 (*
 (* This old version of hnf uses betadeltaiota instead of itself (resp
@@ -882,8 +882,9 @@ let whd_simpl_orelse_delta_but_fix env sigma c =
               | CoFix _ | Fix _ -> s'
 	      | _ -> redrec (applist(c, stack)))
 	| None -> s'
-    else s'
-  in applist (redrec c)
+    else s' in
+  let simpfun = clos_norm_flags betaiota env sigma in
+  simpfun (applist (redrec c))
 
 let hnf_constr = whd_simpl_orelse_delta_but_fix
 
-- 
cgit v1.2.3