From 32a24e55a8e38cd5db37224575269eb4355fdb30 Mon Sep 17 00:00:00 2001
From: mohring
Date: Tue, 28 Aug 2001 09:02:07 +0000
Subject: Change la constante d'entree de Immediate

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

diff --git a/tactics/auto.ml b/tactics/auto.ml
index 9473e0cf3c..742a6ad238 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -316,9 +316,9 @@ let add_externs name pri pat tacast dbnames =
 
 let make_trivial (name,c) =
   let sigma = Evd.empty and env = Global.env() in
-  let t = type_of env sigma c in
+  let t = hnf_constr env sigma (type_of env sigma c) in
   let hd = head_of_constr_reference (List.hd (head_constr t)) in
-  let ce = mk_clenv_from () (c,hnf_constr env sigma t) in
+  let ce = mk_clenv_from () (c,t) in
   (hd, { hname = name;
 	       pri=1;
                pat = Some (Pattern.pattern_of_constr (clenv_template_type ce).rebus);
-- 
cgit v1.2.3