From b78925e69d3e8b0ff2567bf0574e1bd55b33aa93 Mon Sep 17 00:00:00 2001
From: pboutill
Date: Fri, 20 Jul 2012 14:22:40 +0000
Subject: Fixing test-suite

- bug in r15614: hnf was identity
- fix Print Assumptions
- bug in r15624: Dump glob of Print About only for Glob

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

(limited to 'pretyping')

diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index f2f01c3f74..fa7ca0eb82 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -834,9 +834,9 @@ let whd_simpl_orelse_delta_but_fix env sigma c =
       match reference_opt_value sigma env (destEvalRef constr) with
 	| Some c ->
 	    (match kind_of_term (strip_lam c) with
-              | CoFix _ | Fix _ -> s,[]
+              | CoFix _ | Fix _ -> s'
 	      | _ -> redrec (applist(c, stack)))
-	| None -> s,[]
+	| None -> s'
     else s'
   in applist (redrec c)
 
-- 
cgit v1.2.3