From 8f5a7bbf2e5c64d6badd9e7c39da83d07b9c6f40 Mon Sep 17 00:00:00 2001
From: barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Wed, 15 Sep 2004 10:21:40 +0000
Subject: put empty_env in hint clause (vo were becoming huge!)

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

diff --git a/tactics/auto.ml b/tactics/auto.ml
index c32130d2c..45fc35d4b 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -15,6 +15,7 @@ open Nameops
 open Term
 open Termops
 open Sign
+open Environ
 open Inductive
 open Evd
 open Reduction
@@ -209,13 +210,13 @@ let make_apply_entry env sigma (eapply,verbose) name (c,cty) =
            { hname = name;
 	     pri = nb_hyp cty + nmiss;
              pat = Some pat;
-             code = ERes_pf(c,ce) })
+             code = ERes_pf(c,{ce with templenv=empty_env}) })
         end else 
 	  (hd,
            { hname = name;
 	     pri = nb_hyp cty;
              pat = Some pat;
-             code = Res_pf(c,ce) })
+             code = Res_pf(c,{ce with templenv=empty_env}) })
     | _ -> failwith "make_apply_entry"
  
 (* eap is (e,v) with e=true if eapply and v=true if verbose 
@@ -264,7 +265,7 @@ let make_trivial env sigma (name,c) =
   (hd, { hname = name;
 	       pri=1;
                pat = Some (Pattern.pattern_of_constr (clenv_type ce));
-               code=Res_pf_THEN_trivial_fail(c,ce) })
+               code=Res_pf_THEN_trivial_fail(c,{ce with templenv=empty_env}) })
 
 open Vernacexpr
 
-- 
cgit v1.2.3