Modules dans COQ\!\!\!\!

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

14 files changed, 279 insertions, 169 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index 256914d4c..08953ffe0 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -30,10 +30,11 @@ open Tactics
 open Tacticals
 open Clenv
 open Hiddentac
+open Libnames
+open Nametab
 open Libobject
 open Library
 open Printer
-open Nametab
 open Declarations
 open Tacexpr
 
@@ -161,34 +162,7 @@ let _ = Summary.declare_summary "search"
 
  
 (**************************************************************************)
-(*               declaration of the AUTOHINT library object               *)
-(**************************************************************************)
-
-(* If the database does not exist, it is created *)
-(* TODO: should a warning be printed in this case ?? *)
-let add_hint dbname hintlist = 
-  try 
-    let db = searchtable_map dbname in
-    let db' = Hint_db.add_list hintlist db in
-    searchtable_add (dbname,db')
-  with Not_found -> 
-    let db = Hint_db.add_list hintlist Hint_db.empty in
-    searchtable_add (dbname,db)
-
-let cache_autohint (_,(name,hintlist)) =
-  try add_hint name hintlist with _ -> anomaly "Auto.add_hint"
-
-let export_autohint x = Some x
-
-let (inAutoHint,outAutoHint) =
-  declare_object ("AUTOHINT",
-                  { load_function = (fun _ -> ());
-                    cache_function = cache_autohint;
-		    open_function = cache_autohint;
-                    export_function = export_autohint })
-
-(**************************************************************************)
-(*                     The "Hint" vernacular command                      *)
+(*             Auxiliary functions to prepare AUTOHINT objects            *)
 (**************************************************************************)
 
 let rec nb_hyp c = match kind_of_term c with
@@ -261,22 +235,6 @@ let make_resolve_hyp env sigma (hname,_,htyp) =
     | Failure _ -> []
     | e when Logic.catchable_exception e -> anomaly "make_resolve_hyp"
 
-let add_resolves env sigma clist dbnames =
-  List.iter 
-    (fun dbname ->
-       Lib.add_anonymous_leaf
-	 (inAutoHint
-	    (dbname,
-     	     (List.flatten
-		(List.map
-		   (fun (name,c) -> 
-		      let ty = type_of env sigma c in
-		      let verbose = Options.is_verbose() in
-		      make_resolves env sigma name (true,verbose) (c,ty)) clist
-		))
-	    )))
-    dbnames
-
 (* REM : in most cases hintname = id *)
 let make_unfold (hintname, ref) =
   (Pattern.label_of_ref ref,
@@ -285,12 +243,6 @@ let make_unfold (hintname, ref) =
      pat = None;
      code = Unfold_nth ref })
 
-let add_unfolds l dbnames =
-  List.iter 
-    (fun dbname ->
-       Lib.add_anonymous_leaf (inAutoHint (dbname, List.map make_unfold l)))
-    dbnames
-
 let make_extern name pri pat tacast = 
   let hdconstr = try_head_pattern pat in 
   (hdconstr,
@@ -299,6 +251,126 @@ let make_extern name pri pat tacast =
      pat = Some pat;
      code= Extern tacast })
 
+let make_trivial env sigma (name,c) =
+  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,t) in
+  (hd, { hname = name;
+	       pri=1;
+               pat = Some (Pattern.pattern_of_constr (clenv_template_type ce).rebus);
+               code=Res_pf_THEN_trivial_fail(c,ce) })
+
+open Vernacexpr
+
+(**************************************************************************)
+(*               declaration of the AUTOHINT library object               *)
+(**************************************************************************)
+
+let eager o = ref (Lazy.Value o)
+
+(* If the database does not exist, it is created *)
+(* TODO: should a warning be printed in this case ?? *)
+let add_hint dbname hintlist = 
+  try 
+    let db = searchtable_map dbname in
+    let db' = Hint_db.add_list hintlist db in
+    searchtable_add (dbname,db')
+  with Not_found -> 
+    let db = Hint_db.add_list hintlist Hint_db.empty in
+    searchtable_add (dbname,db)
+
+let cache_autohint (_,(name,l_hintlist)) =
+  try add_hint name (Lazy.force l_hintlist) with _ -> anomaly "Auto.add_hint"
+
+let subst_autohint (_,subst,((name,l_hintlist) as obj)) = 
+  let recalc_hints hintlist =
+    let env = Global.env() and sigma = Evd.empty in
+    let recalc_hint ((_,data) as hint) =
+      match data.code with
+	| Res_pf (c,_) ->
+	    let c' = Term.subst_mps subst c in
+	      if c==c' then hint else
+		make_apply_entry env sigma (false,false) 
+		  data.hname (c', type_of env sigma c')
+	| ERes_pf (c,_) ->
+	    let c' = Term.subst_mps subst c in
+	      if c==c' then hint else
+		make_apply_entry env sigma (true,false) 
+		  data.hname (c', type_of env sigma c')
+	| Give_exact c ->
+	    let c' = Term.subst_mps subst c in
+	      if c==c' then hint else
+		make_exact_entry data.hname (c',type_of env sigma c')
+	| Res_pf_THEN_trivial_fail (c,_) ->
+	    let c' = Term.subst_mps subst c in
+	      if c==c' then hint else
+		make_trivial env sigma (data.hname,c')
+	| Unfold_nth ref -> 
+	    let ref' = subst_global subst ref in
+	      if ref==ref' then hint else
+		make_unfold (data.hname,ref')
+	| Extern _ ->
+	    anomaly "Extern hints cannot be substituted!!!"
+    in
+      list_smartmap recalc_hint hintlist
+  in
+  let hintlist = Lazy.force l_hintlist in
+    try
+      let hintlist' = recalc_hints hintlist in
+	if hintlist'==hintlist then
+	  obj
+	else
+	  (name,eager hintlist')
+    with
+	_ -> (name,lazy (recalc_hints hintlist))
+
+let classify_autohint (_,((name,l_hintlist) as obj)) =
+  match Lazy.force l_hintlist with
+      [] -> Dispose   
+    | (_,{code=Extern _})::_ -> Keep obj (* TODO! should be changed *)
+    | _ -> Substitute obj
+
+let export_autohint x = Some x
+
+let (inAutoHint,outAutoHint) =
+  declare_object {(default_object "AUTOHINT") with
+                    cache_function = cache_autohint;
+		    load_function = (fun _ -> cache_autohint);
+		    subst_function = subst_autohint;
+		    classify_function = classify_autohint;
+                    export_function = export_autohint }
+
+
+(**************************************************************************)
+(*                     The "Hint" vernacular command                      *)
+(**************************************************************************)
+let add_resolves env sigma clist dbnames =
+  List.iter 
+    (fun dbname ->
+       Lib.add_anonymous_leaf
+	 (inAutoHint
+	    (dbname,
+	     let l =
+     	       List.flatten
+		 (List.map
+		    (fun (name,c) -> 
+		       let ty = type_of env sigma c in
+		       let verbose = Options.is_verbose() in
+			 make_resolves env sigma name (true,verbose) (c,ty)) clist
+		 )
+	     in
+	       eager l
+	    )))
+    dbnames
+
+
+let add_unfolds l dbnames =
+  List.iter 
+    (fun dbname -> Lib.add_anonymous_leaf 
+       (inAutoHint (dbname, eager (List.map make_unfold l))))
+    dbnames
+
+
 let add_extern name pri (patmetas,pat) tacast dbname =
   (* We check that all metas that appear in tacast have at least
      one occurence in the left pattern pat *)
@@ -312,28 +384,58 @@ let add_extern name pri (patmetas,pat) tacast dbname =
 	  (str "The meta-variable ?" ++ int i ++ str" is not bound")
     | []  ->
 	Lib.add_anonymous_leaf
-	  (inAutoHint(dbname, [make_extern name pri pat tacast]))
+	  (inAutoHint(dbname, eager [make_extern name pri pat tacast]))
 
 let add_externs name pri pat tacast dbnames = 
   List.iter (add_extern name pri pat tacast) dbnames
 
-let make_trivial (name,c) =
-  let sigma = Evd.empty and env = Global.env() 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,t) in
-  (hd, { hname = name;
-	       pri=1;
-               pat = Some (Pattern.pattern_of_constr (clenv_template_type ce).rebus);
-               code=Res_pf_THEN_trivial_fail(c,ce) })
 
-let add_trivials l dbnames =
+let add_trivials env sigma l dbnames =
   List.iter
     (fun dbname ->
-       Lib.add_anonymous_leaf (inAutoHint(dbname, List.map make_trivial l)))
+       Lib.add_anonymous_leaf (
+	 inAutoHint(dbname, eager (List.map (make_trivial env sigma) l))))
     dbnames
 
-open Vernacexpr
+
+let add_hints dbnames h =
+  let dbnames = if dbnames = [] then ["core"] else dbnames in match h with
+  | HintsResolve lhints ->	
+      let env = Global.env() and sigma = Evd.empty in
+      let f (n,c) = 
+	let c = Astterm.interp_constr sigma env c in
+	let n = match n with
+	  | None -> basename (sp_of_global None (Declare.reference_of_constr c))
+	  | Some n -> n in
+	(n,c) in
+      add_resolves env sigma (List.map f lhints) dbnames
+  | HintsImmediate lhints ->
+      let env = Global.env() and sigma = Evd.empty in
+      let f (n,c) = 
+	let c = Astterm.interp_constr sigma env c in
+	let n = match n with
+	  | None -> basename (sp_of_global None (Declare.reference_of_constr c))
+	  | Some n -> n in
+	(n,c) in
+      add_trivials env sigma (List.map f lhints) dbnames
+  | HintsUnfold lhints ->
+      let f (n,locqid) =
+	let r = Nametab.global locqid in
+	let n = match n with
+	  | None -> basename (sp_of_global None r)
+	  | Some n -> n in
+	(n,r) in
+      add_unfolds (List.map f lhints) dbnames
+  | HintsConstructors (hintname, qid) ->
+      let env = Global.env() and sigma = Evd.empty in
+      let isp = global_inductive qid in
+      let consnames = (snd (Global.lookup_inductive isp)).mind_consnames in
+      let lcons = list_tabulate (fun i -> mkConstruct (isp,i+1)) (Array.length consnames) in
+      let lcons = List.map2 (fun id c -> (id,c)) (Array.to_list consnames) lcons in
+      add_resolves env sigma lcons dbnames
+  | HintsExtern (hintname, pri, patcom, tacexp) ->
+      let pat =	Astterm.interp_constrpattern Evd.empty (Global.env()) patcom in
+      add_externs hintname pri pat tacexp dbnames
 
 (**************************************************************************)
 (*                    Functions for printing the hints                    *)
@@ -437,45 +539,6 @@ let print_searchtable () =
        print_hint_db db)
     !searchtable
 
-let add_hints dbnames h =
-  let dbnames = if dbnames = [] then ["core"] else dbnames in match h with
-  | HintsResolve lhints ->	
-      let env = Global.env() and sigma = Evd.empty in
-      let f (n,c) = 
-	let c = Astterm.interp_constr sigma env c in
-	let n = match n with
-	  | None -> basename (sp_of_global env (Declare.reference_of_constr c))
-	  | Some n -> n in
-	(n,c) in
-      add_resolves env sigma (List.map f lhints) dbnames
-  | HintsImmediate lhints ->
-      let env = Global.env() and sigma = Evd.empty in
-      let f (n,c) = 
-	let c = Astterm.interp_constr sigma env c in
-	let n = match n with
-	  | None -> basename (sp_of_global env (Declare.reference_of_constr c))
-	  | Some n -> n in
-	(n,c) in
-      add_trivials (List.map f lhints) dbnames
-  | HintsUnfold lhints ->
-      let f (n,locqid) =
-	let r = Nametab.global locqid in
-	let n = match n with
-	  | None -> basename (sp_of_global (Global.env()) r)
-	  | Some n -> n in
-	(n,r) in
-      add_unfolds (List.map f lhints) dbnames
-  | HintsConstructors (hintname, qid) ->
-      let env = Global.env() and sigma = Evd.empty in
-      let isp = global_inductive qid in
-      let consnames = (snd (Global.lookup_inductive isp)).mind_consnames in
-      let lcons = list_tabulate (fun i -> mkConstruct (isp,i+1)) (Array.length consnames) in
-      let lcons = List.map2 (fun id c -> (id,c)) (Array.to_list consnames) lcons in
-      add_resolves env sigma lcons dbnames
-  | HintsExtern (hintname, pri, patcom, tacexp) ->
-      let pat =	Astterm.interp_constrpattern Evd.empty (Global.env()) patcom in
-      add_externs hintname pri pat tacexp dbnames
-
 (**************************************************************************)
 (*                           Automatic tactics                            *)
 (**************************************************************************)
@@ -811,7 +874,7 @@ let default_superauto g = superauto !default_search_depth [] [] g
 
 let interp_to_add gl locqid =
   let r = Nametab.global locqid in
-  let id = basename (sp_of_global (Global.env()) r) in
+  let id = basename (sp_of_global None r) in
   (next_ident_away id (pf_ids_of_hyps gl), Declare.constr_of_reference r)
 
 let gen_superauto nopt l a b gl =
@@ -822,4 +885,3 @@ let gen_superauto nopt l a b gl =
 let h_superauto no l a b =
   Refiner.abstract_tactic (TacSuperAuto (no,l,a,b)) (gen_superauto no l a b)
 
-
diff --git a/tactics/auto.mli b/tactics/auto.mli
index c5266bc58..c887c1bb4 100644
--- a/tactics/auto.mli
+++ b/tactics/auto.mli
@@ -19,7 +19,7 @@ open Clenv
 open Pattern
 open Environ
 open Evd
-open Nametab
+open Libnames
 (*i*)
   
 type auto_tactic = 
diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml
index 75c7509ac..ad4da1235 100644
--- a/tactics/autorewrite.ml
+++ b/tactics/autorewrite.ml
@@ -61,7 +61,6 @@ let autorewrite tac_main lbas =
        tclTHEN tac (one_base tac_main bas)) tclIDTAC lbas))
 
 (* Functions necessary to the library object declaration *)
-let load_hintrewrite _ = ()
 let cache_hintrewrite (_,(rbase,lrl)) =
   List.iter
     (fun (c,b,t) -> Hashtbl.add !rewtab rbase (c,b,Tacinterp.interp t)) lrl
@@ -69,12 +68,10 @@ let export_hintrewrite x = Some x
 
 (* Declaration of the Hint Rewrite library object *)
 let (in_hintrewrite,out_hintrewrite)=
-  Libobject.declare_object
-    ("HINT_REWRITE",
-     { Libobject.load_function = load_hintrewrite;
-       Libobject.open_function = cache_hintrewrite;
+  Libobject.declare_object {(Libobject.default_object "HINT_REWRITE") with
+       Libobject.open_function = (fun i o -> if i=1 then cache_hintrewrite o);
        Libobject.cache_function = cache_hintrewrite;
-       Libobject.export_function = export_hintrewrite })
+       Libobject.export_function = export_hintrewrite }
 
 (* To add rewriting rules to a base *)
 let add_rew_rules base lrul =
diff --git a/tactics/dhyp.ml b/tactics/dhyp.ml
index d73677617..92db61f07 100644
--- a/tactics/dhyp.ml
+++ b/tactics/dhyp.ml
@@ -200,11 +200,10 @@ type destructor_data_object = identifier * destructor_data
 
 let ((inDD : destructor_data_object->obj),
      (outDD : obj->destructor_data_object)) =
-  declare_object ("DESTRUCT-HYP-CONCL-DATA",
-                  { load_function = (fun _ -> ());
+  declare_object {(default_object "DESTRUCT-HYP-CONCL-DATA") with
                     cache_function = cache_dd;
-		    open_function = cache_dd;
-                    export_function = export_dd })
+		    open_function = (fun i o -> if i=1 then cache_dd o);
+                    export_function = export_dd }
     
 let add_destructor_hint na loc pat pri code =
   begin match loc, code with
diff --git a/tactics/elim.ml b/tactics/elim.ml
index cbe18ba36..b4f718fbd 100644
--- a/tactics/elim.ml
+++ b/tactics/elim.ml
@@ -14,6 +14,7 @@ open Names
 open Term
 open Termops
 open Environ
+open Libnames
 open Reduction
 open Inductiveops
 open Proof_type
@@ -103,7 +104,7 @@ let head_in gls indl t =
   with Not_found -> false
        
 let inductive_of = function
-  | Nametab.IndRef ity -> ity
+  | IndRef ity -> ity
   | r ->
       errorlabstrm "Decompose"
         (Printer.pr_global r ++ str " is not an inductive type")
diff --git a/tactics/equality.ml b/tactics/equality.ml
index fdb579729..bec72973d 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -1231,18 +1231,15 @@ let add_list_rules rbase lrl =
 let rules_of_base rbase = List.rev (Gmapl.find rbase !rew_tab)
 
 (*Functions necessary to the library object declaration*)
-let load_autorewrite_rule _ = ()
 let cache_autorewrite_rule (_,(rbase,lrl)) = add_list_rules rbase lrl
 let export_autorewrite_rule x = Some x
 
 (*Declaration of the AUTOREWRITE_RULE library object*)
 let (in_autorewrite_rule,out_autorewrite_rule)=
-  Libobject.declare_object
-    ("AUTOREWRITE_RULE",
-     { Libobject.load_function = load_autorewrite_rule;
-       Libobject.open_function = cache_autorewrite_rule;
+  Libobject.declare_object {(Libobject.default_object "AUTOREWRITE_RULE") with
+       Libobject.open_function = (fun i o -> if i=1 then cache_autorewrite_rule o);
        Libobject.cache_function = cache_autorewrite_rule;
-       Libobject.export_function = export_autorewrite_rule })
+       Libobject.export_function = export_autorewrite_rule }
 
 (****The tactic****)
 
diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index 1a83dbb5d..36e0fa23f 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -19,6 +19,7 @@ open Evd
 open Printer
 open Reductionops
 open Declarations
+open Entries
 open Inductiveops
 open Environ
 open Tacmach
@@ -244,10 +245,10 @@ let add_inversion_lemma name env sigma t sort dep inv_op =
   let invProof = inversion_scheme env sigma t sort dep inv_op in
   let _ = 
     declare_constant name
-    (ConstantEntry { const_entry_body = invProof;
+    (DefinitionEntry { const_entry_body = invProof;
                      const_entry_type = None;
                      const_entry_opaque = false }, 
-     Nametab.NeverDischarge)
+     Libnames.NeverDischarge)
   in ()
 
 (* open Pfedit *)
diff --git a/tactics/setoid_replace.ml b/tactics/setoid_replace.ml
index a147997ba..1962318f9 100644
--- a/tactics/setoid_replace.ml
+++ b/tactics/setoid_replace.ml
@@ -15,6 +15,8 @@ open Reductionops
 open Term
 open Termops
 open Names
+open Entries
+open Libnames
 open Nameops
 open Util
 open Pp
@@ -51,7 +53,7 @@ let constant dir s =
     try 
       Declare.global_reference_in_absolute_module dir id
   with Not_found ->
-    anomaly ("Setoid: cannot find "^(Nametab.string_of_qualid (Nametab.make_qualid dir id)))
+    anomaly ("Setoid: cannot find "^(string_of_qualid (make_qualid dir id)))
 
 let global_constant dir s =
   let dir = make_dirpath
@@ -60,7 +62,7 @@ let global_constant dir s =
     try 
       Declare.global_reference_in_absolute_module dir id
   with Not_found ->
-    anomaly ("Setoid: cannot find "^(Nametab.string_of_qualid (Nametab.make_qualid dir id)))
+    anomaly ("Setoid: cannot find "^(string_of_qualid (make_qualid dir id)))
 
 let current_constant id =
   try
@@ -97,6 +99,21 @@ let setoid_table_add (s,th) = setoid_table := Gmap.add s th !setoid_table
 let setoid_table_find s = Gmap.find s !setoid_table
 let setoid_table_mem s = Gmap.mem s !setoid_table
 
+let subst_setoid subst setoid = 
+  let set_a' = subst_mps subst setoid.set_a in
+  let set_aeq' = subst_mps subst setoid.set_aeq in
+  let set_th' = subst_mps subst setoid.set_th in
+    if set_a' == setoid.set_a
+      && set_aeq' == setoid.set_aeq
+      && set_th' == setoid.set_th
+    then
+      setoid
+    else
+      { set_a = set_a' ;
+	set_aeq = set_aeq' ;
+	set_th = set_th' ;
+      }
+      
 let equiv_list () = List.map (fun x -> x.set_aeq) (Gmap.rng !setoid_table)
 
 let _ = 
@@ -110,13 +127,19 @@ let _ =
 
 let (setoid_to_obj, obj_to_setoid)=
   let cache_set (_,(s, th)) = setoid_table_add (s,th)
+  and subst_set (_,subst,(s,th as obj)) =
+    let s' = subst_mps subst s in
+    let th' = subst_setoid subst th in
+      if s' == s && th' == th then obj else
+	(s',th')
   and export_set x = Some x 
   in 
-    declare_object ("setoid-theory",
-		    { cache_function = cache_set;
-		      load_function = (fun _ -> ());
-		      open_function = cache_set;
-		      export_function = export_set})
+    declare_object {(default_object "setoid-theory") with
+		      cache_function = cache_set;
+		      open_function = (fun i o -> if i=1 then cache_set o);
+		      subst_function = subst_set;
+		      classify_function = (fun (_,x) -> Substitute x);
+		      export_function = export_set}
 
 (******************************* Table of declared morphisms ********************)
 
@@ -128,6 +151,23 @@ let morphism_table_add (m,c) = morphism_table := Gmap.add m c !morphism_table
 let morphism_table_find m = Gmap.find m !morphism_table
 let morphism_table_mem m = Gmap.mem m !morphism_table
 
+let subst_morph subst morph = 
+  let lem' = subst_mps subst morph.lem in
+  let arg_types' = list_smartmap (subst_mps subst) morph.arg_types in
+  let lem2' = option_smartmap (subst_mps subst) morph.lem2 in
+    if lem' == morph.lem
+      && arg_types' == morph.arg_types
+      && lem2' == morph.lem2
+    then
+      morph
+    else
+      { lem = lem' ;
+	profil = morph.profil ;
+	arg_types = arg_types' ;
+	lem2 = lem2' ;
+      }
+
+
 let _ = 
   Summary.declare_summary "morphism-table"
     { Summary.freeze_function = (fun () -> !morphism_table);
@@ -139,13 +179,19 @@ let _ =
 
 let (morphism_to_obj, obj_to_morphism)=
   let cache_set (_,(m, c)) = morphism_table_add (m, c)
+  and subst_set (_,subst,(m,c as obj)) = 
+    let m' = subst_mps subst m in
+    let c' = subst_morph subst c in
+      if m' == m && c' == c then obj else
+	(m',c')
   and export_set x = Some x 
   in 
-    declare_object ("morphism-definition",
-		    { cache_function = cache_set;
-		      load_function = (fun _ -> ());
-		      open_function = cache_set;
-		      export_function = export_set})
+    declare_object {(default_object "morphism-definition") with
+		      cache_function = cache_set;
+		      open_function = (fun i o -> if i=1 then cache_set o);
+		      subst_function = subst_set;
+		      classify_function = (fun (_,x) -> Substitute x);
+		      export_function = export_set}
 
 (************************** Adding a setoid to the database *********************)
 
@@ -238,15 +284,15 @@ let add_setoid a aeq th =
 	    let eq_ext_name = gen_eq_lem_name () in 
 	    let eq_ext_name2 = gen_eq_lem_name () in 
 	    let _ = Declare.declare_constant eq_ext_name
-		      ((ConstantEntry {const_entry_body = eq_morph; 
+		      ((DefinitionEntry {const_entry_body = eq_morph; 
 		                       const_entry_type = None;
                                        const_entry_opaque = true}),
-		       Nametab.NeverDischarge) in
+		       Libnames.NeverDischarge) in
 	    let _ = Declare.declare_constant eq_ext_name2
-		      ((ConstantEntry {const_entry_body = eq_morph2; 
+		      ((DefinitionEntry {const_entry_body = eq_morph2; 
 				       const_entry_type = None;
                                        const_entry_opaque = true}),
-		       Nametab.NeverDischarge) in
+		       Libnames.NeverDischarge) in
 	    let eqmorph = (current_constant eq_ext_name) in
 	    let eqmorph2 = (current_constant eq_ext_name2) in
 	      (Lib.add_anonymous_leaf
@@ -290,10 +336,10 @@ let check_is_dependent t n =
 
 let gen_lem_name m = match kind_of_term m with 
   | Var id -> add_suffix id "_ext"
-  | Const sp -> add_suffix (basename sp) "_ext"
-  | Ind (sp, i) -> add_suffix (basename sp) ((string_of_int i)^"_ext")
-  | Construct ((sp,i),j) -> add_suffix
-      (basename sp) ((string_of_int i)^(string_of_int j)^"_ext")
+  | Const kn -> add_suffix (id_of_label (label kn)) "_ext"
+  | Ind (kn, i) -> add_suffix (id_of_label (label kn)) ((string_of_int i)^"_ext")
+  | Construct ((kn,i),j) -> add_suffix
+      (id_of_label (label kn)) ((string_of_int i)^(string_of_int j)^"_ext")
   | _ -> errorlabstrm "New Morphism" (str "The term " ++ prterm m ++ str "is not a known name")
 
 let gen_lemma_tail m lisset body n =
@@ -359,7 +405,7 @@ let new_morphism m id hook =
 	let lem = (gen_compat_lemma env m body args_t poss) in
 	let lemast = (ast_of_constr true env lem) in
 	new_edited id m poss;
-	start_proof_com (Some id) (false,Nametab.NeverDischarge) lemast hook;
+	start_proof_com (Some id) (false,Libnames.NeverDischarge) lemast hook;
 	(Options.if_verbose Vernacentries.show_open_subgoals ()))
 
 let rec sub_bool l1 n = function
@@ -451,10 +497,10 @@ let add_morphism lem_name (m,profil) =
 	 (let lem_2 = gen_lem_iff env m mext args_t poss in
 	  let lem2_name = add_suffix lem_name "2" in
 	  let _ = Declare.declare_constant lem2_name
-		    ((ConstantEntry {const_entry_body = lem_2; 
+		    ((DefinitionEntry {const_entry_body = lem_2; 
 				     const_entry_type = None;
                                      const_entry_opaque = true}),
-		     Nametab.NeverDischarge) in
+		     Libnames.NeverDischarge) in
 	  let lem2 = (current_constant lem2_name) in
 	    (Lib.add_anonymous_leaf
 	       (morphism_to_obj (m, 
@@ -472,7 +518,7 @@ let add_morphism lem_name (m,profil) =
 				lem2 = None}))));
       Options.if_verbose ppnl (prterm m ++str " is registered as a morphism")   
 let morphism_hook stre ref =
-  let pf_id = basename (sp_of_global (Global.env()) ref) in
+  let pf_id = basename (sp_of_global None ref) in
   if (is_edited pf_id)
   then 
     (add_morphism pf_id (what_edited pf_id); no_more_edited pf_id)
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index d3721d015..27eb73d0a 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -12,6 +12,7 @@ open Astterm
 open Closure
 open RedFlags
 open Declarations
+open Entries
 open Dyn
 open Libobject
 open Pattern
@@ -22,6 +23,7 @@ open Tacred
 open Util
 open Names
 open Nameops
+open Libnames
 open Nametab
 open Pfedit
 open Proof_type
@@ -121,7 +123,7 @@ let make_hyps = List.map (fun (id,_,typ) -> (id,body_of_type typ))
 (* Transforms an id into a constr if possible *)
 let constr_of_id ist id =
   match ist.goalopt with
-  | None -> construct_reference ist.env id
+  | None -> construct_reference (Some (Environ.named_context ist.env)) id
   | Some goal ->
     let hyps = pf_hyps goal in
     if mem_named_context id hyps then
@@ -196,7 +198,7 @@ let look_for_interp = Hashtbl.find interp_tab
 
 let find_reference ist qid =
   (* We first look for a variable of the current proof *)
-  match Nametab.repr_qualid qid, ist.goalopt with
+  match repr_qualid qid, ist.goalopt with
     | (d,id),Some gl when repr_dirpath d = [] & List.mem id (pf_ids_of_hyps gl)
 	-> VarRef id
     | _ -> Nametab.locate qid
@@ -308,7 +310,7 @@ let glob_hyp_or_metanum ist = function
   | MetaNum (loc,n) -> MetaNum (loc,glob_metanum ist loc n)
 
 let glob_qualid_or_metanum ist = function
-  | AN (loc,qid) -> AN (loc,qualid_of_sp (sp_of_global (Global.env())(Nametab.global (loc,qid))))
+  | AN (loc,qid) -> AN (loc,qualid_of_sp (sp_of_global None (Nametab.global (loc,qid))))
   | MetaNum (loc,n) -> MetaNum (loc,glob_metanum ist loc n)
 
 let glob_reference ist (_,qid as locqid) =
@@ -317,7 +319,7 @@ let glob_reference ist (_,qid as locqid) =
     if dir = empty_dirpath && List.mem id (fst ist) then qid
     else raise Not_found
   with Not_found ->
-    qualid_of_sp (sp_of_global (Global.env()) (Nametab.global locqid))
+    qualid_of_sp (sp_of_global None (Nametab.global locqid))
 
 let glob_ltac_qualid ist (loc,qid as locqid) =
   try qualid_of_sp (locate_tactic qid)
@@ -824,7 +826,7 @@ let constr_to_id loc c =
   else invalid_arg_loc (loc, "Not an identifier")
 
 let constr_to_qid loc c =
-  try qualid_of_sp (sp_of_global (Global.env ()) (reference_of_constr c))
+  try qualid_of_sp (sp_of_global None (reference_of_constr c))
   with _ -> invalid_arg_loc (loc, "Not a global reference")
 
 (* Check for LetTac *)
@@ -1706,15 +1708,14 @@ let register_tacdef (sp,td) =
 
 let cache_md (_,defs) =
   (* Needs a rollback if something goes wrong *)
-  List.iter (fun (sp,_) -> Nametab.push_tactic_path sp) defs;
+  List.iter (fun (sp,_) -> Nametab.push_tactic (Until 1) sp) defs;
   List.iter add (List.map register_tacdef defs)
 
 let (inMD,outMD) =
-  declare_object ("TAC-DEFINITION",
-    {cache_function  = cache_md;
-     load_function   = (fun _ -> ());
-     open_function   = cache_md;
-     export_function = (fun x -> Some x)})
+  declare_object {(default_object "TAC-DEFINITION") with
+     cache_function  = cache_md;
+     open_function   = (fun i o -> if i=1 then cache_md o);
+     export_function = (fun x -> Some x)}
 
 (* Adds a definition for tactics in the table *)
 let make_absolute_name (loc,id) =
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index b6fea7dc2..08004e971 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -18,6 +18,7 @@ open Declarations
 open Inductive
 open Reduction
 open Environ
+open Libnames
 open Declare
 open Refiner
 open Tacmach
@@ -314,7 +315,7 @@ let general_elim_then_using
       | _ ->
 	  let name_elim =
 	    match kind_of_term elim with
-	      | Const sp -> string_of_path sp
+	      | Const kn -> string_of_kn kn
 	      | Var id -> string_of_id id
 	      | _ -> "\b"
 	  in
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 690f1f4f9..37da503fd 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -20,6 +20,7 @@ open Inductive
 open Inductiveops
 open Reductionops
 open Environ
+open Libnames
 open Declare
 open Evd
 open Pfedit
@@ -906,8 +907,8 @@ let find_eliminator c gl =
   let env = pf_env gl in
   let (ind,t) = reduce_to_quantified_ind env (project gl) (pf_type_of gl c) in
   let s = elimination_sort_of_goal gl in
-  try Indrec.lookup_eliminator ind s 
-  with Not_found -> 
+    Indrec.lookup_eliminator ind s 
+(*  with Not_found -> 
     let dir, base = repr_path (path_of_inductive env ind) in
     let id = Indrec.make_elimination_ident base s in
     errorlabstrm "default_elim"
@@ -917,7 +918,7 @@ let find_eliminator c gl =
          pr_id base ++ spc () ++ str "on sort " ++
          spc () ++ print_sort (new_sort_in_family s) ++
 	 str " is probably not allowed")
-
+(* lookup_eliminator prints the message *) *)
 let default_elim (c,lbindc) gl = 
   general_elim (c,lbindc) (find_eliminator c gl,NoBindings) gl
 
@@ -926,6 +927,7 @@ let elim (c,lbindc) elim gl =
   | Some (elimc,lbindelimc) -> general_elim (c,lbindc) (elimc,lbindelimc) gl
   | None -> general_elim (c,lbindc) (find_eliminator c gl,NoBindings) gl 
 
+
 (* The simplest elimination tactic, with no substitutions at all. *)
 
 let simplest_elim c = default_elim (c,NoBindings)
@@ -1001,7 +1003,7 @@ let general_elim_in id (c,lbindc) (elimc,lbindelimc) gl =
 
 (* We recompute recargs because we are not sure the elimination lemma
 comes from a canonically generated one *)
-
+(* dead code ?
 let rec is_rec_arg env sigma indpath t =
   try
     let (ind_sp,_) = find_mrectype env sigma t in
@@ -1014,7 +1016,7 @@ let rec recargs indpath env sigma t =
 	(is_rec_arg env sigma indpath t)
 	::(recargs indpath (push_rel_assum (na,t) env) sigma c2)
     | _ -> []
-
+*)
 let induct_discharge old_style mind statuslists cname destopt avoid ra gl =
   let (lstatus,rstatus) = statuslists in
   let tophyp = ref None in
@@ -1598,7 +1600,7 @@ let abstract_subproof name tac gls =
   in
   if occur_existential concl then error "Abstract cannot handle existentials";
   let lemme =
-    start_proof na (false,Nametab.NeverDischarge) current_sign concl (fun _ _ -> ());
+    start_proof na (false,NeverDischarge) current_sign concl (fun _ _ -> ());
     let _,(const,(_,strength),_) =
       try
 	by (tclCOMPLETE (tclTHEN (tclDO (List.length sign) intro) tac)); 
@@ -1607,10 +1609,10 @@ let abstract_subproof name tac gls =
       with e when catchable_exception e -> 
 	(delete_current_proof(); raise e)
     in   (* Faudrait un peu fonctionnaliser cela *)
-    let cd = Safe_typing.ConstantEntry const in
+    let cd = Entries.DefinitionEntry const in
     let sp = Declare.declare_constant na (cd,strength) in
     let newenv = Global.env() in
-    Declare.constr_of_reference (ConstRef sp)
+    Declare.constr_of_reference (ConstRef (snd sp))
   in
   exact_no_check 
     (applist (lemme,
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 14d479362..9d1f61616 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -21,6 +21,7 @@ open Evar_refiner
 open Clenv
 open Tacred
 open Tacticals
+open Libnames
 open Tacexpr
 open Nametab
 open Rawterm
diff --git a/tactics/tauto.ml4 b/tactics/tauto.ml4
index f4f8452fa..dc28eb48c 100644
--- a/tactics/tauto.ml4
+++ b/tactics/tauto.ml4
@@ -14,6 +14,7 @@ open Ast
 open Coqast
 open Hipattern
 open Names
+open Libnames
 open Pp
 open Proof_type
 open Tacticals
diff --git a/tactics/termdn.ml b/tactics/termdn.ml
index 2d0f49f4e..d3acf6e68 100644
--- a/tactics/termdn.ml
+++ b/tactics/termdn.ml
@@ -14,6 +14,7 @@ open Nameops
 open Term
 open Pattern
 open Rawterm
+open Libnames
 open Nametab
 
 (* Discrimination nets of terms.