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

1 files 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);