Auto: avoid storing clausenv (and hence env, evar_map, universes) in vo

 It appears that registration of hints is the only place (at least
 when compiling stdlib) where Univ.universes (the graph of universes)
 is stored in vo. More precisely, a Hint Resolve will place in vo
 a pri_auto_tactic, which may contain some clausenv, which contain
 both a env and a evar_map, each of them containing a Univ.universes
 In fact, even env and evar_map are also never stored in vo apart
 from hints registration.

 Currently, there's nothing wrong in this storing of env / evar_map /
 universes. In fact, it seems that every stored universes are actually
 empty. Same for env, thanks to awkward lines { cl with env=empty_env }.
 But this may hinder potential evolutions of Univ.universes toward a
 private per-session representation. Conclusion: it is cleaner
 (and not that hard) to store a Term.types instead of the clausenv
 in vo, and reconstitute the clausenv at Require-time. On a compilation
 of the stdlib, the time effect is hardly noticable (<1%).

 NB: a Univ.universes is also stored in initial.coq, but this is a
 different story (Write State ...)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14611 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 11 insertions, 9 deletions

diff --git a/tactics/auto.mli b/tactics/auto.mli
index 8556b453fc..1bff2eef85 100644
--- a/tactics/auto.mli
+++ b/tactics/auto.mli
@@ -22,30 +22,32 @@ open Mod_subst
 
 (** Auto and related automation tactics *)
 
-type auto_tactic =
-  | Res_pf     of constr * clausenv    (** Hint Apply *)
-  | ERes_pf    of constr * clausenv    (** Hint EApply *)
+type 'a auto_tactic =
+  | Res_pf     of constr * 'a    (** Hint Apply *)
+  | ERes_pf    of constr * 'a    (** Hint EApply *)
   | Give_exact of constr
-  | Res_pf_THEN_trivial_fail of constr * clausenv (** Hint Immediate *)
+  | Res_pf_THEN_trivial_fail of constr * 'a (** Hint Immediate *)
   | Unfold_nth of evaluable_global_reference          (** Hint Unfold *)
   | Extern     of Tacexpr.glob_tactic_expr   (** Hint Extern *)
 
 open Glob_term
 
-type pri_auto_tactic = {
+type 'a gen_auto_tactic = {
   pri   : int;            (** A number between 0 and 4, 4 = lower priority *)
   pat   : constr_pattern option; (** A pattern for the concl of the Goal *)
-  name  : global_reference option; (** A potential name to refer to the hint *) 
-  code  : auto_tactic;    (** the tactic to apply when the concl matches pat *)
+  name  : global_reference option; (** A potential name to refer to the hint *)
+  code  : 'a auto_tactic; (** the tactic to apply when the concl matches pat *)
 }
 
+type pri_auto_tactic = clausenv gen_auto_tactic
+
 type stored_data = int * pri_auto_tactic
 
 type search_entry
 
 (** The head may not be bound. *)
 
-type hint_entry = global_reference option * pri_auto_tactic
+type hint_entry = global_reference option * types gen_auto_tactic
 
 module Hint_db :
   sig
@@ -231,7 +233,7 @@ val gen_trivial : open_constr list -> hint_db_name list option -> tactic
 val full_trivial : open_constr list -> tactic
 val h_trivial : open_constr list -> hint_db_name list option -> tactic
 
-val pr_autotactic : auto_tactic -> Pp.std_ppcmds
+val pr_autotactic : 'a auto_tactic -> Pp.std_ppcmds
 
 (** {6 The following is not yet up to date -- Papageno. } *)