Suppression option immediate_discharge; nettoyage de Declare et conséquences

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

41 files changed, 177 insertions, 381 deletions

diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 47e56e3b0..33a26c800 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -338,11 +338,6 @@ let cci_inductive locals env env_ar kind finite inds cst =
       Idset.empty inds
   in
   let hyps = keep_hyps env ids (named_context env) in
-  let inds' =
-    if Options.immediate_discharge then
-      List.map (abstract_inductive ntypes hyps) inds
-    else
-      inds in
   let one_packet i (params,nparams,id,ar,cnames,issmall,isunit,lc) =
     let recargs = listrec_mconstr env_ar ntypes params nparams i lc in
     let isunit = isunit && ntypes = 1 && (not (is_recursive [0] recargs)) in
@@ -373,7 +368,7 @@ let cci_inductive locals env env_ar kind finite inds cst =
       mind_params_ctxt = params }
   in
   let sp_hyps = List.map (fun (id,b,t) -> (List.assoc id locals,b,t)) hyps in
-  let packets = Array.of_list (list_map_i one_packet 1 inds') in
+  let packets = Array.of_list (list_map_i one_packet 1 inds) in
   { mind_kind = kind;
     mind_ntypes = ntypes;
     mind_hyps = sp_hyps;
diff --git a/kernel/instantiate.ml b/kernel/instantiate.ml
index c1e864523..0191b6391 100644
--- a/kernel/instantiate.ml
+++ b/kernel/instantiate.ml
@@ -49,11 +49,8 @@ let instantiate_evar sign c args =
     replace_vars inst c
 
 let instantiate_constr sign c args =
-  if Options.immediate_discharge then
-    c
-  else
-    let sign = List.map (fun (sp,b,t) -> (basename sp,b,t)) sign in
-    instantiate sign c args
+  let sign = List.map (fun (sp,b,t) -> (basename sp,b,t)) sign in
+  instantiate sign c args
 
 let instantiate_type sign tty args =
   type_app (fun c -> instantiate_constr sign c args) tty
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 6eba04182..a6ae51f89 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -273,12 +273,6 @@ let add_global_declaration sp env locals (body,typ,cst) op =
     | Some b ->
         Idset.union (global_vars_set env b) (global_vars_set env typ) in
   let hyps = keep_hyps env ids (named_context env) in
-  let body, typ =
-    if Options.immediate_discharge then
-      option_app (fun c -> it_mkNamedLambda_or_LetIn c hyps) body,
-      it_mkNamedProd_or_LetIn typ hyps
-    else
-      body,typ in
   let sp_hyps = List.map (fun (id,b,t) -> (List.assoc id locals, b, t)) hyps in
   let cb = {
     const_kind = kind_of_path sp;
diff --git a/kernel/sign.ml b/kernel/sign.ml
index 0d7168c00..0899cf5e6 100644
--- a/kernel/sign.ml
+++ b/kernel/sign.ml
@@ -70,8 +70,7 @@ let instance_from_section_context sign =
     | [] -> [] in
   Array.of_list (inst_rec sign)
 let instance_from_section_context x =
-  if Options.immediate_discharge then [||]
-  else instance_from_section_context x
+  instance_from_section_context x
 
 (*s Signatures of ordered optionally named variables, intended to be
    accessed by de Bruijn indices *)
diff --git a/lib/options.ml b/lib/options.ml
index d5efe7fef..a8adcdb74 100644
--- a/lib/options.ml
+++ b/lib/options.ml
@@ -64,6 +64,3 @@ let without_mes_ambig f x =
 let unsafe_set = ref Stringset.empty
 let add_unsafe s = unsafe_set := Stringset.add s !unsafe_set
 let is_unsafe s = Stringset.mem s !unsafe_set
-
-(* To deal with two kinds of discharge *)
-let immediate_discharge = false
diff --git a/lib/options.mli b/lib/options.mli
index 84c60c9dd..bf73cfcdf 100644
--- a/lib/options.mli
+++ b/lib/options.mli
@@ -38,5 +38,3 @@ val without_mes_ambig : ('a -> 'b) -> 'a -> 'b
 
 val add_unsafe : string -> unit
 val is_unsafe : string -> bool
-
-val immediate_discharge : bool
diff --git a/library/declare.ml b/library/declare.ml
index 19c7323c9..c2ac0ce45 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -368,37 +368,6 @@ let context_of_global_reference = function
   | IndRef (sp,_) -> (Global.lookup_mind sp).mind_hyps
   | ConstructRef ((sp,_),_) -> (Global.lookup_mind sp).mind_hyps
 
-(*
-let global_sp_operator env sp id =
-  try
-
-  with Not_found -> 
-    let mib = 
-    mind_oper_of_id sp id mib, mib.mind_hyps
-*)
-
-let rec occur_section_variable sp = function
-  | (_,sp')::_ when sp = sp' -> true
-  | _::l -> occur_section_variable sp l
-  | [] -> false
-
-let rec quantify_extra_hyps c = function
-  | (sp,None,t)::hyps ->
-      mkNamedLambda (basename sp) t (quantify_extra_hyps c hyps)
-  (* Buggé car id n'apparaît pas dans les instances des constantes dans c *)
-  (* et id n'est donc pas substitué dans ces constantes *)
-  | (sp,Some b,t)::hyps ->
-      mkNamedLetIn (basename sp) b t (quantify_extra_hyps c hyps)
-  | [] -> c
-
-let find_common_hyps_then_abstract c hyps' hyps =
-  let rec find = function
-    | (sp,_,_) :: hyps when occur_section_variable sp hyps' -> find hyps
-    | hyps -> quantify_extra_hyps c hyps in
-  find (List.rev hyps)
-
-let section_variable_paths () = snd !vartab
-
 let find_section_variable id =
   let l =
     Spmap.fold
@@ -407,7 +376,14 @@ let find_section_variable id =
   match l with
     | [] -> raise Not_found
     | [sp] -> sp
-    | _ -> error "Arghh, you blasted me with several variables of same name"
+    | _ -> anomaly "Several section variables with same base name"
+
+let reference_of_constr c = match kind_of_term c with
+  | IsConst sp -> ConstRef sp
+  | IsMutInd ind_sp -> IndRef ind_sp
+  | IsMutConstruct cstr_cp -> ConstructRef cstr_cp
+  | IsVar id -> VarRef (find_section_variable id)
+  |  _ -> raise Not_found
 
 let last_section_hyps dir =
   List.fold_right
@@ -418,32 +394,7 @@ let rec find_var id = function
   | [] -> raise Not_found
   | sp::l -> if basename sp = id then sp else find_var id l
 
-let implicit_section_args ref =
-  if Options.immediate_discharge then
-    let hyps = context_of_global_reference ref in
-    let hyps0 = section_variable_paths () in
-    let rec keep acc = function
-      | (sp,None,_)::hyps ->
-	  let acc = if List.mem sp hyps0 then sp::acc else acc in
-	  keep acc hyps
-      | (_,Some _,_)::hyps -> keep acc hyps
-      | [] -> acc
-    in keep [] hyps
-  else []
-
-let section_hyps ref =
-  let hyps = context_of_global_reference ref in
-  let hyps0 = section_variable_paths () in
-  let rec keep acc = function
-    | (sp,b,_ as d)::hyps ->
-	let acc = if List.mem sp hyps0 then (sp,b=None)::acc else acc in
-	keep acc hyps
-    | [] -> acc
-  in keep [] hyps
-
 let extract_instance ref args =
-  if Options.immediate_discharge then args
-  else
   let hyps = context_of_global_reference ref in
   let hyps0 = current_section_context () in
   let na = Array.length args in
@@ -455,50 +406,37 @@ let extract_instance ref args =
     | [] -> Array.of_list acc
   in peel (na-1) [] hyps
 
-let constr_of_reference _ _ ref =
-if Options.immediate_discharge then
-  match ref with
-    | VarRef sp -> mkVar (basename sp)
-    | ConstRef sp -> mkConst sp
-    | ConstructRef sp -> mkMutConstruct sp
-    | IndRef sp -> mkMutInd sp
-else
-  let hyps = context_of_global_reference ref in
-  let hyps0 = current_section_context () in
-  let body = match ref with
-    | VarRef sp -> mkVar (basename sp)
-    | ConstRef sp -> mkConst sp
-    | ConstructRef sp -> mkMutConstruct sp
-    | IndRef sp -> mkMutInd sp
-  in
-  find_common_hyps_then_abstract body hyps0 hyps
+let constr_of_reference = function
+  | VarRef sp -> mkVar (basename sp)
+  | ConstRef sp -> mkConst sp
+  | ConstructRef sp -> mkMutConstruct sp
+  | IndRef sp -> mkMutInd sp
 
-let construct_absolute_reference env sp =
-  constr_of_reference Evd.empty env (Nametab.absolute_reference sp)
+let construct_absolute_reference sp =
+  constr_of_reference (Nametab.absolute_reference sp)
 
-let construct_qualified_reference env qid =
+let construct_qualified_reference qid =
   let ref = Nametab.locate qid in
-  constr_of_reference Evd.empty env ref
+  constr_of_reference ref
 
-let construct_reference env kind id =
+let construct_reference env id =
   try
     mkVar (let _ = Environ.lookup_named id env in id)
   with Not_found ->
-    let ref = Nametab.sp_of_id kind id in
-    constr_of_reference Evd.empty env ref
+    let ref = Nametab.sp_of_id CCI id in
+    constr_of_reference ref
 
 let global_qualified_reference qid =
-  construct_qualified_reference (Global.env()) qid
+  construct_qualified_reference qid
 
 let global_absolute_reference sp = 
-  construct_absolute_reference (Global.env()) sp
+  construct_absolute_reference sp
 
 let global_reference_in_absolute_module dir id = 
-  constr_of_reference Evd.empty (Global.env())
-    (Nametab.locate_in_absolute_module dir id)
+  constr_of_reference (Nametab.locate_in_absolute_module dir id)
 
-let global_reference kind id = 
-  construct_reference (Global.env()) kind id
+let global_reference id = 
+  construct_reference (Global.env()) id
 
 let dirpath_of_global = function
   | VarRef sp -> dirpath sp
@@ -513,7 +451,7 @@ let is_section_variable = function
 let is_global id =
   try 
     let osp = Nametab.locate (make_qualid [] id) in
-    (* Compatibilité V6.3: Les variables de section de sont pas globales
+    (* Compatibilité V6.3: Les variables de section ne sont pas globales
     not (is_section_variable osp) && *)
     list_prefix_of (dirpath_of_global osp) (Lib.cwd())
   with Not_found -> 
@@ -533,22 +471,7 @@ let path_of_inductive_path (sp,tyi) =
     let (pa,_,k) = repr_path sp in 
     Names.make_path pa (mip.mind_typename) k 
 
-(* Util *)
-let instantiate_inductive_section_params t ind =
-  if Options.immediate_discharge then 
-  let sign = section_hyps (IndRef ind) in
-  let rec inst s ctxt t =
-    let k = kind_of_term t in
-    match (ctxt,k) with
-    | (sp,true)::ctxt, IsLambda(_,_,t) ->
-	inst ((mkVar (basename sp))::s) ctxt t
-    | (sp,false)::ctxt, IsLetIn(_,_,_,t) -> 
-	inst ((mkVar (basename sp))::s) ctxt t
-    | [], _ -> substl s t
-    | _ -> anomaly"instantiate_params: term and ctxt mismatch"
-  in inst [] sign t
-  else t
-(* Eliminations. *)
+(*s Eliminations. *)
 
 let eliminations =
   [ (InProp,"_ind") ; (InSet,"_rec") ; (InType,"_rect") ]
@@ -563,9 +486,6 @@ let make_elimination_ident id s = add_suffix id (elimination_suffix s)
 let declare_one_elimination mispec =
   let mindstr = string_of_id (mis_typename mispec) in
   let declare na c =
-    (* Hack to get const_hyps right in the declaration *)
-    let c = instantiate_inductive_section_params c (mis_inductive mispec)
-    in
     let _ = declare_constant (id_of_string na)
       (ConstantEntry
         { const_entry_body = c;
@@ -607,9 +527,9 @@ let lookup_eliminator env ind_sp s =
   let id = add_suffix base (elimination_suffix s) in
   (* Try first to get an eliminator defined in the same section as the *)
   (* inductive type *)
-  try construct_absolute_reference env (Names.make_path dir id k)
+  try construct_absolute_reference (Names.make_path dir id k)
   with Not_found ->
   (* Then try to get a user-defined eliminator in some other places *)
   (* using short name (e.g. for "eq_rec") *)
-  construct_reference env (kind_of_path path) id
+  construct_reference env id
   
diff --git a/library/declare.mli b/library/declare.mli
index 6918c99db..be5678f7f 100644
--- a/library/declare.mli
+++ b/library/declare.mli
@@ -81,32 +81,31 @@ val variable_strength : variable -> strength
 val find_section_variable : identifier -> variable
 val last_section_hyps : dir_path -> identifier list
 
-(*s [global_reference k id] returns the object corresponding to
-    the name [id] in the global environment. It may be a constant, 
-    an inductive, a construtor or a variable. It is instanciated
-    on the current environment of variables. [Nametab.sp_of_id] is used
-    to find the corresponding object. 
-    [construct_reference] is a version which looks for variables in a 
-    given environment instead of looking in the current global environment. *)
+(*s Global references *)
 
 val context_of_global_reference : global_reference -> section_context
-val instantiate_inductive_section_params : constr -> inductive -> constr
-val implicit_section_args : global_reference -> section_path list
 val extract_instance : global_reference -> constr array -> constr array
 
-val constr_of_reference :
-  'a Evd.evar_map -> Environ.env -> global_reference -> constr
+(* Turn a global reference into a construction *)
+val constr_of_reference : global_reference -> constr
+
+(* Turn a construction denoting a global into a reference;
+   raise [Not_found] if not a global *)
+val reference_of_constr : constr -> global_reference
 
 val global_qualified_reference : Nametab.qualid -> constr
 val global_absolute_reference : section_path -> constr
 val global_reference_in_absolute_module : dir_path -> identifier -> constr
 
-val construct_qualified_reference : Environ.env -> Nametab.qualid -> constr
-val construct_absolute_reference : Environ.env -> section_path -> constr
+val construct_qualified_reference : Nametab.qualid -> constr
+val construct_absolute_reference : section_path -> constr
 
 (* This should eventually disappear *)
-val global_reference : path_kind -> identifier -> constr
-val construct_reference : Environ.env -> path_kind -> identifier -> constr
+(*  [construct_reference] returns the object corresponding to
+    the name [id] in the global environment. It looks also for variables in a 
+    given environment instead of looking in the current global environment. *)
+val global_reference : identifier -> constr
+val construct_reference : Environ.env -> identifier -> constr
 
 val is_global : identifier -> bool
 
diff --git a/library/nametab.ml b/library/nametab.ml
index 6cd43c392..643c4ff16 100755
--- a/library/nametab.ml
+++ b/library/nametab.ml
@@ -240,6 +240,16 @@ let absolute_reference sp =
 let locate_in_absolute_module dir id =
   absolute_reference (make_path dir id CCI)
 
+let global loc qid =
+  try match extended_locate qid with
+    | TrueGlobal ref -> ref
+    | SyntacticDef _ -> 
+        error
+          ("Unexpected reference to a syntactic definition: "
+           ^(string_of_qualid qid))
+  with Not_found ->
+    error_global_not_found_loc loc qid
+
 let exists_cci sp =
   try let _ = locate_cci (qualid_of_sp sp) in true
   with Not_found -> false
diff --git a/library/nametab.mli b/library/nametab.mli
index f34895bef..5150c18b1 100755
--- a/library/nametab.mli
+++ b/library/nametab.mli
@@ -65,6 +65,10 @@ val constant_sp_of_id : identifier -> section_path
 
 val locate : qualid -> global_reference
 
+(* This function is used to transform a qualified identifier into a
+   global reference, with a nice error message in case of failure *)
+val global : loc -> qualid -> global_reference
+
 (* This locates also syntactic definitions *)
 val extended_locate : qualid -> extended_global_reference
 
diff --git a/parsing/astterm.ml b/parsing/astterm.ml
index efac22bc7..736ed0663 100644
--- a/parsing/astterm.ml
+++ b/parsing/astterm.ml
@@ -30,10 +30,6 @@ open Nametab
 (*Takes a list of variables which must not be globalized*)
 let from_list l = List.fold_right Idset.add l Idset.empty
 
-let rec adjust_implicits n = function
-  | p::l -> if p<=n then adjust_implicits n l else (p-n)::adjust_implicits n l
-  | [] -> []
-
 (* when an head ident is not a constructor in pattern *)
 let mssg_hd_is_not_constructor s =
   [< 'sTR "The symbol "; pr_id s; 'sTR " should be a constructor" >]
@@ -201,26 +197,20 @@ let ast_to_global loc c =
   match c with
     | ("CONST", [sp]) ->
 	let ref = ConstRef (ast_to_sp sp) in
-	let hyps = implicit_section_args ref in
-	let section_args = List.map (fun id -> RRef (loc, VarRef id)) hyps in
 	let imps = implicits_of_global ref in
-	RRef (loc, ref), section_args, adjust_implicits (List.length hyps) imps
+	RRef (loc, ref), imps
     | ("MUTIND", [sp;Num(_,tyi)]) -> 
 	let ref = IndRef (ast_to_sp sp, tyi) in
-	let hyps = implicit_section_args ref in
-	let section_args = List.map (fun id -> RRef (loc, VarRef id)) hyps in
 	let imps = implicits_of_global ref in
-	RRef (loc, ref), section_args, adjust_implicits (List.length hyps) imps
+	RRef (loc, ref), imps
     | ("MUTCONSTRUCT", [sp;Num(_,ti);Num(_,n)]) ->
 	let ref = ConstructRef ((ast_to_sp sp,ti),n) in
-	let hyps = implicit_section_args ref in
-	let section_args = List.map (fun id -> RRef (loc, VarRef id)) hyps in
 	let imps = implicits_of_global ref in
-	RRef (loc, ref), section_args, adjust_implicits (List.length hyps) imps
+	RRef (loc, ref), imps
     | ("EVAR", [(Num (_,ev))]) ->
-	REvar (loc, ev), [], []
+	REvar (loc, ev), []
     | ("SYNCONST", [sp]) ->
-	Syntax_def.search_syntactic_definition (ast_to_sp sp), [], []
+	Syntax_def.search_syntactic_definition (ast_to_sp sp), []
     | _ -> anomaly_loc (loc,"ast_to_global",
 			[< 'sTR "Bad ast for this global a reference">])
 
@@ -251,7 +241,7 @@ let ast_to_var (env,impls) (vars1,vars2) loc id =
 	let ref = VarRef (Lib.make_path id CCI) in
 	implicits_of_global ref
       with _ -> []
-  in RVar (loc, id), [], imps
+  in RVar (loc, id), imps
 
 (**********************************************************************)
 
@@ -271,12 +261,10 @@ let rawconstr_of_qualid env vars loc qid =
   (* Is it a global reference or a syntactic definition? *)
   try match Nametab.extended_locate qid with
   | TrueGlobal ref ->
-    let hyps = implicit_section_args ref in
-    let section_args = List.map (fun id -> RRef (loc, VarRef id)) hyps in
     let imps = implicits_of_global ref in
-    RRef (loc, ref), section_args, adjust_implicits (List.length hyps) imps
+    RRef (loc, ref), imps
   | SyntacticDef sp ->
-    set_loc_of_rawconstr loc (Syntax_def.search_syntactic_definition sp),[],[]
+    set_loc_of_rawconstr loc (Syntax_def.search_syntactic_definition sp), []
   with Not_found ->
     error_global_not_found_loc loc qid
 
@@ -366,12 +354,10 @@ let check_capture loc s ty = function
 let ast_to_rawconstr sigma env allow_soapp lvar =
   let rec dbrec (ids,impls as env) = function
     | Nvar(loc,s) ->
-	let f, hyps, _ = rawconstr_of_var env lvar loc s in
-	if hyps = [] then f else RApp (loc, f, hyps)
+	fst (rawconstr_of_var env lvar loc s)
 
     | Node(loc,"QUALID", l) ->
-	let f, hyps, _ = rawconstr_of_qualid env lvar loc (interp_qualid l) in
-	if hyps = [] then f else RApp (loc, f, hyps)
+        fst (rawconstr_of_qualid env lvar loc (interp_qualid l))
   
     | Node(loc,"FIX", (Nvar (locid,iddef))::ldecl) ->
 	let (lf,ln,lA,lt) = ast_to_fix ldecl in
@@ -416,7 +402,7 @@ let ast_to_rawconstr sigma env allow_soapp lvar =
 	RApp (loc,dbrec env f,ast_to_args env args)
 
     | Node(loc,"APPLIST", f::args) ->
-	let (c, hyps, impargs) =
+	let (c, impargs) =
 	  match f with
 	    | Node(locs,"QUALID",p) ->
 		rawconstr_of_qualid env lvar locs (interp_qualid p)
@@ -424,9 +410,9 @@ let ast_to_rawconstr sigma env allow_soapp lvar =
 		   ("CONST"|"EVAR"|"MUTIND"|"MUTCONSTRUCT"|"SYNCONST" as key),
 		   l) ->
 		ast_to_global loc (key,l)
-	    | _ -> (dbrec env f, [], [])
+	    | _ -> (dbrec env f, [])
         in
-	  RApp (loc, c, hyps @ (ast_to_impargs env impargs args))
+	  RApp (loc, c, ast_to_impargs env impargs args)
 
     | Node(loc,"CASES", p:: Node(_,"TOMATCH",tms):: eqns) ->
 	let po = match p with 
@@ -456,8 +442,7 @@ let ast_to_rawconstr sigma env allow_soapp lvar =
 	  
     (* This case mainly parses things build in a quotation *)
     | Node(loc,("CONST"|"EVAR"|"MUTIND"|"MUTCONSTRUCT"|"SYNCONST" as key),l) ->
-	let f, hyps, _ = ast_to_global loc (key,l) in
-	if hyps = [] then f else RApp (loc, f, hyps)	
+	fst (ast_to_global loc (key,l))
 
     | Node(loc,"CAST", [c1;c2]) ->	   
 	RCast (loc,dbrec env c1,dbrec env c2)
diff --git a/parsing/coqlib.ml b/parsing/coqlib.ml
index dca396ea2..4d3e5ce23 100644
--- a/parsing/coqlib.ml
+++ b/parsing/coqlib.ml
@@ -51,8 +51,7 @@ let reference dir s =
   with Not_found ->
     anomaly ("Coqlib: cannot find "^(string_of_qualid (make_qualid dir id)))
 
-let constant dir s =
-  Declare.constr_of_reference Evd.empty (Global.env()) (reference dir s)
+let constant dir s = Declare.constr_of_reference (reference dir s)
 
 type coq_sigma_data = {
   proj1 : constr;
diff --git a/parsing/g_basevernac.ml4 b/parsing/g_basevernac.ml4
index 2a447a910..6dbaabc1c 100644
--- a/parsing/g_basevernac.ml4
+++ b/parsing/g_basevernac.ml4
@@ -91,7 +91,7 @@ GEXTEND Gram
       | IDENT "Print" -> <:ast< (PRINT) >>
       | IDENT "Print"; IDENT "Hint"; "*" 
 	                    -> <:ast< (PrintHint) >>
-      | IDENT "Print"; IDENT "Hint"; s = identarg ->
+      | IDENT "Print"; IDENT "Hint"; s = qualidarg ->
           <:ast< (PrintHintId $s) >>
       | IDENT "Print"; IDENT "Hint" ->
           <:ast< (PrintHintGoal) >>
@@ -172,7 +172,8 @@ GEXTEND Gram
       | IDENT "Print"; IDENT "Graph" -> <:ast< (PrintGRAPH) >>
       | IDENT "Print"; IDENT "Classes" -> <:ast< (PrintCLASSES) >>
       | IDENT "Print"; IDENT "Coercions" -> <:ast< (PrintCOERCIONS) >>
-      | IDENT "Print"; IDENT "Coercion"; IDENT "Paths"; c = identarg; d = identarg ->
+      | IDENT "Print"; IDENT "Coercion"; IDENT "Paths";
+        c = qualidarg; d = qualidarg ->
           <:ast< (PrintPATH $c $d) >>
 
       | IDENT "SearchIsos"; com = constrarg ->
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 3bec62837..f98746a25 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -214,7 +214,7 @@ GEXTEND Gram
       | ":" -> "" ] ]
   ;
   onescheme:
-    [ [ id = identarg; ":="; dep = dep; indid = identarg; IDENT "Sort";
+    [ [ id = identarg; ":="; dep = dep; indid = qualidarg; IDENT "Sort";
         s = sortarg ->
           <:ast< (VERNACARGLIST $id $dep $indid $s) >> ] ]
   ;
diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml
index 7c6dad215..5f804f3f2 100644
--- a/parsing/prettyp.ml
+++ b/parsing/prettyp.ml
@@ -577,33 +577,23 @@ let print_coercions () =
   [< prlist_with_sep pr_spc
        (fun (_,(_,v)) -> [< print_coercion_value v >]) (coercions()) >]
   
-let cl_of_id id = 
-  match string_of_id id with
-    | "FUNCLASS" -> CL_FUN
-    | "SORTCLASS" -> CL_SORT
-    | _ -> let v = Declare.global_reference CCI id in
-	   let cl,_ = constructor_at_head v in 
-	   cl
-
-let index_cl_of_id id =
+let index_of_class cl =
   try 
-    let cl = cl_of_id id in
-    let i,_ = class_info cl in 
-    i
+    fst (class_info cl)
   with _ -> 
-    errorlabstrm "index_cl_of_id"
-      [< 'sTR(string_of_id id); 'sTR" is not a defined class" >]
+    errorlabstrm "index_of_class"
+      [< 'sTR(string_of_class cl); 'sTR" is not a defined class" >]
 
-let print_path_between ids idt = 
-  let i = (index_cl_of_id ids) in
-  let j = (index_cl_of_id idt) in
+let print_path_between cls clt = 
+  let i = index_of_class cls in
+  let j = index_of_class clt in
   let p = 
     try 
       lookup_path_between (i,j) 
     with _ -> 
       errorlabstrm "index_cl_of_id"
-        [< 'sTR"No path between ";'sTR(string_of_id ids); 
-	   'sTR" and ";'sTR(string_of_id ids) >]
+        [< 'sTR"No path between ";'sTR(string_of_class cls); 
+	   'sTR" and ";'sTR(string_of_class clt) >]
   in
   print_path ((i,j),p)
 
diff --git a/parsing/prettyp.mli b/parsing/prettyp.mli
index b84c56634..a50a8371f 100644
--- a/parsing/prettyp.mli
+++ b/parsing/prettyp.mli
@@ -52,7 +52,7 @@ i*)
 val print_graph : unit -> std_ppcmds
 val print_classes : unit -> std_ppcmds
 val print_coercions : unit -> std_ppcmds
-val print_path_between : identifier -> identifier -> std_ppcmds
+val print_path_between : Classops.cl_typ -> Classops.cl_typ -> std_ppcmds
 
 
 val inspect : int -> std_ppcmds
diff --git a/parsing/search.ml b/parsing/search.ml
index e0dc3b7a4..fc069f41e 100644
--- a/parsing/search.ml
+++ b/parsing/search.ml
@@ -48,7 +48,7 @@ let rec head_const c = match kind_of_term c with
 let crible (fn : global_reference -> env -> constr -> unit) ref =
   let env = Global.env () in
   let imported = Library.opened_modules() in
-  let const = constr_of_reference Evd.empty env ref in 
+  let const = constr_of_reference ref in 
   let crible_rec sp lobj =
     match object_tag lobj with
       | "VARIABLE" ->
diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index 5a88e62dc..18bb39099 100755
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -21,19 +21,6 @@ open Rawterm
 
 (* usage qque peu general: utilise aussi dans record *)
 
-type cte_typ = 
-  | NAM_Section_Variable of variable
-  | NAM_Constant of constant
-  | NAM_Inductive of inductive
-  | NAM_Constructor of constructor
-
-let cte_of_constr c = match kind_of_term c with
-  | IsConst sp -> ConstRef sp
-  | IsMutInd ind_sp -> IndRef ind_sp
-  | IsMutConstruct cstr_cp -> ConstructRef cstr_cp
-  | IsVar id -> VarRef (Declare.find_section_variable id)
-  |  _ -> raise Not_found
-
 type cl_typ = 
   | CL_SORT 
   | CL_FUN
diff --git a/pretyping/classops.mli b/pretyping/classops.mli
index 019644e20..c68eba1dd 100644
--- a/pretyping/classops.mli
+++ b/pretyping/classops.mli
@@ -44,7 +44,6 @@ type coe_index
 (* This is the type of paths from a class to another *)
 type inheritance_path = coe_index list
 
-val cte_of_constr : constr -> global_reference
 val coe_of_reference : global_reference -> coe_typ
 
 (*s [declare_class] adds a class to the set of declared classes *)
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index b4df53b8a..e0c1db169 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -99,12 +99,11 @@ let used_of = global_vars_and_consts
 (* Tools for printing of Cases                                              *)
 
 let encode_inductive ref =
-  let indsp =
-      match kind_of_term (constr_of_reference Evd.empty (Global.env()) ref)with
-        | IsMutInd indsp -> indsp
-	| _ -> errorlabstrm "indsp_of_id" 
-	    [< 'sTR ((Global.string_of_global ref)^
-                      " is not an inductive type") >] in
+  let indsp = match ref with
+    | IndRef indsp -> indsp
+    | _ -> errorlabstrm "indsp_of_id"
+        [< 'sTR ((Global.string_of_global ref)^" is not an inductive type") >]
+  in
   let mis = Global.lookup_mind_specif indsp in
   let constr_lengths = Array.map List.length (mis_recarg mis) in
   (indsp,constr_lengths)
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index e221e4945..23bcfd8e4 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -310,7 +310,7 @@ and conv_record env isevars (c,bs,(xs,xs1),(us,us1),(ts,ts1),t) =
 and check_conv_record (t1,l1) (t2,l2) = 
   try
     let {o_DEF=c;o_TABS=bs;o_TPARAMS=xs;o_TCOMPS=us} = 
-      objdef_info (cte_of_constr t1,cte_of_constr t2) in
+      objdef_info (Declare.reference_of_constr t1, Declare.reference_of_constr t2) in
     let xs1,t,ts = 
       match list_chop (List.length xs) l1 with 
 	| xs1,t::ts -> xs1,t,ts
diff --git a/pretyping/pattern.ml b/pretyping/pattern.ml
index 54e67e401..253e3e579 100644
--- a/pretyping/pattern.ml
+++ b/pretyping/pattern.ml
@@ -161,7 +161,7 @@ let matches_core convert pat c =
 
       | PVar v1, IsVar v2 when v1 = v2 -> sigma
 
-      | PRef ref, _ when Declare.constr_of_reference Evd.empty (Global.env()) ref = cT -> sigma
+      | PRef ref, _ when Declare.constr_of_reference ref = cT -> sigma
 
       | PRel n1, IsRel n2 when n1 = n2 -> sigma
 
@@ -184,7 +184,7 @@ let matches_core convert pat c =
 
       | PRef (ConstRef _ as ref), _ when convert <> None ->
 	  let (env,evars) = out_some convert in
-	  let c = Declare.constr_of_reference Evd.empty env ref in
+	  let c = Declare.constr_of_reference ref in
 	  if is_conv env evars c cT then sigma
 	  else raise PatternMatchingFailure
 
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 2cb322bea..c0238dbda 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -165,7 +165,7 @@ let pretype_id loc env lvar id =
 (* Main pretyping function                                               *)
 
 let pretype_ref isevars env lvar ref = 
-  let c = Declare.constr_of_reference (evars_of isevars) env ref in
+  let c = Declare.constr_of_reference ref in
   make_judge c (Retyping.get_type_of env Evd.empty c)
 
 (*
diff --git a/proofs/tacinterp.ml b/proofs/tacinterp.ml
index a77fb84a0..0013fc32f 100644
--- a/proofs/tacinterp.ml
+++ b/proofs/tacinterp.ml
@@ -122,7 +122,7 @@ let constr_of_id id = function
     if mem_named_context id hyps then
       mkVar id
     else
-      let csr = Declare.global_reference CCI id in
+      let csr = global_qualified_reference (make_qualid [] id) in
       (match kind_of_term csr with
       | IsVar _ -> raise Not_found
       | _ -> csr)
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index 8a05e0989..d429b4069 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -82,7 +82,7 @@ let pf_interp_type gls c =
   let evc = project gls in 
   Astterm.interp_type evc (pf_env gls) c
 
-let pf_global gls id = Declare.construct_reference (pf_env gls) CCI id
+let pf_global gls id = Declare.construct_reference (pf_env gls) id
 
 let pf_parse_const gls = compose (pf_global gls) id_of_string
 
diff --git a/tactics/auto.ml b/tactics/auto.ml
index 088e7636a..6bd773698 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -273,10 +273,6 @@ let add_resolves env sigma clist dbnames =
 	    )))
     dbnames
 
-let global qid =
-  try Nametab.locate qid
-  with Not_found -> Nametab.error_global_not_found_loc dummy_loc qid
-
 (* REM : in most cases hintname = id *)
 let make_unfold (hintname, ref) =
   (Pattern.label_of_ref ref,
@@ -340,7 +336,7 @@ let _ =
 	       (function VARG_IDENTIFIER i -> string_of_id i
 		  | _ -> bad_vernac_args "HintUnfold") l in
       	   fun () -> 
-	     let ref = global qid in
+	     let ref = Nametab.global dummy_loc qid in
 	     add_unfolds [(hintname, ref)] dbnames
        | _-> bad_vernac_args "HintUnfold")
     
@@ -381,13 +377,11 @@ let _ =
 	       let isp = destMutInd (Declare.global_qualified_reference qid) in
 	       let conspaths =
 		 mis_conspaths (Global.lookup_mind_specif isp) in
-	       let hyps = Declare.implicit_section_args (IndRef isp) in
-	       let section_args = List.map (fun sp -> mkVar (basename sp)) hyps in
 	       let lcons = 
 		 array_map_to_list
 		   (fun sp ->
 		      let c = Declare.global_absolute_reference sp in
-		      (basename sp, applist (c, section_args)))
+		      (basename sp, c))
 		   conspaths in
 	       let dbnames = if l = [] then ["core"] else 
 	      	 List.map (function VARG_IDENTIFIER i -> string_of_id i
@@ -422,13 +416,11 @@ let _ =
 	     List.map
 	       (function
 		  | VARG_QUALID qid -> 
-		      let ref = global qid in
+		      let ref = Nametab.global dummy_loc qid in
 		      let env = Global.env() in
-		      let c = Declare.constr_of_reference Evd.empty env ref in
-		      let hyps = Declare.implicit_section_args ref in
-		      let section_args = List.map (fun sp -> mkVar (basename sp)) hyps in
+		      let c = Declare.constr_of_reference ref in
 		      let _,i = Nametab.repr_qualid qid in
-		      (i, applist (c,section_args))
+		      (i, c)
 		  | _-> bad_vernac_args "HintsResolve") lh in
 	   let dbnames = if l = [] then ["core"] else 
 	     List.map (function VARG_IDENTIFIER i -> string_of_id i
@@ -445,7 +437,7 @@ let _ =
 	     List.map (function
 			 | VARG_QUALID qid ->
 			     let _,n = Nametab.repr_qualid qid in
-			     (n, global qid)
+			     (n, Nametab.global dummy_loc qid)
 		      	 | _ -> bad_vernac_args "HintsUnfold") lh in
 	   let dbnames = if l = [] then ["core"] else 
 	     List.map (function 
@@ -466,10 +458,8 @@ let _ =
 		      let _,n = Nametab.repr_qualid qid in
 		      let ref = Nametab.locate qid in
 		      let env = Global.env () in
-		      let c = Declare.constr_of_reference Evd.empty env ref in
-		      let hyps = Declare.implicit_section_args ref in
-		      let section_args = List.map (fun sp -> mkVar (basename sp)) hyps in
-		      (n, applist (c, section_args))
+		      let c = Declare.constr_of_reference ref in
+		      (n, c)
 		  | _ -> bad_vernac_args "HintsImmediate") lh in
 	   let dbnames = if l = [] then ["core"] else 
 	     List.map (function 
@@ -517,15 +507,10 @@ let fmt_hint_list_for_head c =
       [< 'sTR"For "; pr_ref_label c; 'sTR" -> "; 'fNL;
 	 hOV 0 (prlist fmt_hints_db valid_dbs) >]
 
-let fmt_hint_id id = 
-  try 
-    let c = Declare.global_reference CCI id in
-    fmt_hint_list_for_head (head_of_constr_reference c)
-  with Not_found -> 
-    [< pr_id id; 'sTR " not declared" >]
+let fmt_hint_ref ref = fmt_hint_list_for_head (label_of_ref ref)
 
 (* Print all hints associated to head id in any database *)
-let print_hint_id id =  pPNL(fmt_hint_id id)
+let print_hint_qid qid =  pPNL(fmt_hint_ref (Nametab.global dummy_loc qid))
 
 let fmt_hint_term cl = 
   try 
@@ -607,7 +592,7 @@ let _ =
 let _ = 
   vinterp_add "PrintHintId"
     (function 
-       | [(VARG_IDENTIFIER id)] -> fun () -> print_hint_id id
+       | [(VARG_QUALID qid)] -> fun () -> print_hint_qid qid
        | _ -> bad_vernac_args "PrintHintId")
 
 (**************************************************************************)
@@ -961,7 +946,7 @@ let interp_to_add gl = function
   | Qualid qid ->
       let _,id = Nametab.repr_qualid qid in
       (next_ident_away id (pf_ids_of_hyps gl), 
-       Declare.constr_of_reference Evd.empty (Global.env()) (global qid))
+       Declare.constr_of_reference (Nametab.global dummy_loc qid))
   | _ -> errorlabstrm "cvt_autoArgs" [< 'sTR "Qualid expected" >]
 
 let dyn_superauto l g = 
diff --git a/tactics/elim.ml b/tactics/elim.ml
index dc0393b06..fed756814 100644
--- a/tactics/elim.ml
+++ b/tactics/elim.ml
@@ -100,7 +100,7 @@ let head_in gls indl t =
        
 let inductive_of_qualid gls qid =
   let c = 
-    try Declare.construct_qualified_reference (pf_env gls) qid
+    try Declare.construct_qualified_reference qid
     with Not_found -> Nametab.error_global_not_found qid
   in
   match kind_of_term c with
diff --git a/tactics/equality.ml b/tactics/equality.ml
index e497fb114..6c3ee44d8 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -56,7 +56,7 @@ let general_rewrite_bindings lft2rgt (c,l) gl =
 	then general_s_rewrite lft2rgt c gl
 	else error "The term provided does not end with an equation" 
     | Some (hdcncl,_) -> 
-        let hdcncls = string_head hdcncl in 
+        let hdcncls = string_of_inductive hdcncl in 
 	let suffix = Declare.elimination_suffix (elimination_sort_of_goal gl)in
         let elim =
 	  if lft2rgt then
@@ -115,20 +115,12 @@ let abstract_replace (eq,sym_eq) (eqt,sym_eqt) c2 c1 unsafe gl =
   else
     error "terms does not have convertible types"
 
-(* Only for internal use *)
-let unsafe_replace c2 c1 gl = 
-  let eq        = (pf_parse_const gl "eq")     in
-  let eqt       = (pf_parse_const gl "eqT")    in 
-  let sym_eq    = (pf_parse_const gl "sym_eq") in
-  let sym_eqt   = (pf_parse_const gl "sym_eqT") in
-  abstract_replace (eq,sym_eq) (eqt,sym_eqt) c2 c1 true gl
-
-let replace c2 c1 gl = 
-  let eq        = (pf_parse_const gl "eq")     in
-  let eqt       = (pf_parse_const gl "eqT")    in 
-  let sym_eq    = (pf_parse_const gl "sym_eq") in
-  let sym_eqt   = (pf_parse_const gl "sym_eqT") in
-  abstract_replace (eq,sym_eq) (eqt,sym_eqt) c2 c1 false gl
+let replace c2 c1 gl =
+  let eq = build_coq_eq_data.eq () in
+  let eq_sym = build_coq_eq_data.sym () in
+  let eqT = build_coq_eqT_data.eq () in
+  let eqT_sym = build_coq_eqT_data.sym () in
+  abstract_replace (eq,eq_sym) (eqT,eqT_sym) c2 c1 false gl
     
 let dyn_replace args gl = 
   match args with 
diff --git a/tactics/equality.mli b/tactics/equality.mli
index 1735ebf1a..b7ec9eb59 100644
--- a/tactics/equality.mli
+++ b/tactics/equality.mli
@@ -57,9 +57,6 @@ val conditional_rewrite_in :
 val abstract_replace : 
   constr * constr -> constr * constr -> constr -> constr -> bool -> tactic
 
-(* Only for internal use *)
-val unsafe_replace : constr -> constr -> tactic
-
 val replace   : constr -> constr -> tactic
 val h_replace : constr -> constr -> tactic
 
diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml
index ae2ed421f..a3bdf52b9 100644
--- a/tactics/hipattern.ml
+++ b/tactics/hipattern.ml
@@ -119,9 +119,9 @@ let is_unit_type t = op2bool (match_with_unit_type t)
 
 (* Checks if a given term is an application of an
    inductive binary relation R, so that R has only one constructor
-   stablishing its reflexivity.  *)
+   establishing its reflexivity.  *)
 
-let match_with_equation  t =
+let match_with_equation t =
   let (hdapp,args) = decomp_app t in
   match (kind_of_term hdapp) with
     | IsMutInd ind -> 
diff --git a/tactics/setoid_replace.ml b/tactics/setoid_replace.ml
index d19c67c18..ea9e9d104 100644
--- a/tactics/setoid_replace.ml
+++ b/tactics/setoid_replace.ml
@@ -56,7 +56,7 @@ let global_constant dir s =
 
 let current_constant id =
   try
-    Declare.global_reference CCI id
+    Declare.global_reference id
   with Not_found ->
     anomaly ("Setoid: cannot find "^(string_of_id id))
 
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 8a8025f12..04d7b10c1 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -57,20 +57,13 @@ let get_pairs_from_bindings =
   in 
   List.map pair_from_binding
 
-let rec string_head_bound x = match kind_of_term x with
-  | IsConst cst -> string_of_id (basename cst)
+let string_of_inductive c = 
+  try match kind_of_term c with
   | IsMutInd ind_sp -> 
       let mispec = Global.lookup_mind_specif ind_sp in 
       string_of_id (mis_typename mispec)
-  | IsMutConstruct (ind_sp,i) ->
-       let mispec = Global.lookup_mind_specif ind_sp in 
-       string_of_id (mis_consnames mispec).(i-1)
-  | IsVar id -> string_of_id id
   | _ -> raise Bound
-
-let string_head c = 
-  try string_head_bound c with Bound -> error "Bound head variable"
-
+  with Bound -> error "Bound head variable"
 
 let rec head_constr_bound t l =
   let t = strip_outer_cast(collapse_appl t) in
@@ -1744,8 +1737,8 @@ let dyn_reflexivity = function
 let symmetry gl =
   match match_with_equation (pf_concl gl) with
     | None -> error "The conclusion is not a substitutive equation" 
-    | Some (hdcncl,args) -> 
-        let hdcncls = string_head hdcncl in
+    | Some (hdcncl,args) ->
+        let hdcncls = string_of_inductive hdcncl in
         begin 
 	  try 
 	    (apply (pf_parse_const gl ("sym_"^hdcncls)) gl)
@@ -1782,9 +1775,9 @@ let dyn_symmetry = function
 
 let transitivity t gl =
   match match_with_equation (pf_concl gl) with
-    | None -> error "The conlcusion is not a substitutive equation" 
+    | None -> error "The conclusion is not a substitutive equation" 
     | Some (hdcncl,args) -> 
-        let hdcncls = string_head hdcncl in
+        let hdcncls = string_of_inductive hdcncl in
         begin
 	  try 
 	    apply_list [(pf_parse_const gl ("trans_"^hdcncls));t] gl 
@@ -1846,7 +1839,7 @@ let abstract_subproof name tac gls =
     in   (* Faudrait un peu fonctionnaliser cela *)
     let sp = Declare.declare_constant na (ConstantEntry const,strength) in
     let newenv = Global.env() in
-    Declare.constr_of_reference Evd.empty newenv (ConstRef sp)
+    Declare.constr_of_reference (ConstRef sp)
   in
   exact_no_check 
     (applist (lemme,
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 8751fcb5c..7205303b2 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -29,12 +29,7 @@ open Tacticals
 val type_clenv_binding : walking_constraints ->
   constr * constr -> constr substitution  -> constr
 
-(*i
-(* [force_reference c] fails if [c] is not a reference *)
-val force_reference   : constr -> constr
-i*)
-
-val string_head       : constr -> string
+val string_of_inductive : constr -> string
 val head_constr       : constr -> constr list
 val head_constr_bound : constr -> constr list -> constr list
 val bad_tactic_args : string -> tactic_arg list -> 'a
diff --git a/toplevel/class.ml b/toplevel/class.ml
index 50c0f33e0..21e1242f8 100644
--- a/toplevel/class.ml
+++ b/toplevel/class.ml
@@ -82,7 +82,7 @@ let rec arity_sort a = match kind_of_term a with
 (* try_add_class : Names.identifier ->
   Term.constr -> (cl_typ * int) option -> bool -> int * Libobject.strength *)
 
-let try_add_class v (cl,p) streopt check_exist = 
+let try_add_class (cl,p) streopt check_exist = 
   if check_exist & class_exists cl then
     errorlabstrm "try_add_new_class" 
       [< 'sTR (string_of_class cl) ; 'sTR " is already a class" >];
@@ -96,7 +96,7 @@ let try_add_class v (cl,p) streopt check_exist =
 (* try_add_new_class : Names.identifier -> unit *)
 
 let try_add_new_class ref stre =
-  let v = constr_of_reference Evd.empty (Global.env()) ref in
+  let v = constr_of_reference ref in
   let env = Global.env () in
   let t = Retyping.get_type_of env Evd.empty v in
   let p1 =
@@ -108,7 +108,7 @@ let try_add_new_class ref stre =
            'sTR " does not end with a sort" >] 
   in
   let cl = fst (constructor_at_head v) in
-  let _ = try_add_class v (cl,p1) (Some stre) true in () 
+  let _ = try_add_class (cl,p1) (Some stre) true in () 
 
 (* Coercions *)
 
@@ -173,7 +173,7 @@ let check_class v cl p =
       with Not_found -> raise (CoercionError (NotAClass cl))
     in
     check_fully_applied cl p p1;
-    try_add_class v (cl,p1) None false
+    try_add_class (cl,p1) None false
 
 (* check that the computed target is the provided one *)
 let check_target clt = function
@@ -294,7 +294,7 @@ let error_not_transparent source =
 let build_id_coercion idf_opt source =
   let env = Global.env () in
   let vs = match source with
-    | CL_CONST sp -> constr_of_reference Evd.empty env (ConstRef sp)
+    | CL_CONST sp -> mkConst sp
     | _ -> error_not_transparent source in
   let c = match Instantiate.constant_opt_value env (destConst vs) with
     | Some c -> c
@@ -349,7 +349,7 @@ lorque source est None alors target est None aussi.
 
 let add_new_coercion_core coef stre source target isid =
   let env = Global.env () in
-  let v = constr_of_reference Evd.empty env coef in
+  let v = constr_of_reference coef in
   let vj = Retyping.get_judgment_of env Evd.empty v in
   if coercion_exists coef then raise (CoercionError AlreadyExists);
   let lp = prods_of (vj.uj_type) in
@@ -408,7 +408,7 @@ type coercion_entry =
 let add_new_coercion (ref,stre,isid,cls,clt,n) =
   (* Un peu lourd, tout cela pour trouver l'instance *)
   let env = Global.env () in
-  let v = constr_of_reference Evd.empty env ref in
+  let v = constr_of_reference ref in
   let vj = Retyping.get_judgment_of env Evd.empty v in
   declare_coercion ref vj stre isid cls clt n
 
@@ -458,11 +458,6 @@ let process_class sec_sp ids_to_discard x =
           let newsp = Lib.make_path spid CCI in
 	  let hyps = (Global.lookup_constant sp).const_hyps in
 	  let n = count_extra_abstractions hyps ids_to_discard in
-(*
-          let v = global_reference CCI spid in
-          let t = Retyping.get_type_of env Evd.empty v in
-          let p = arity_sort t in
-*)
           (CL_CONST newsp,{cl_strength=stre;cl_param=p+n})
         else 
 	  x
@@ -472,11 +467,6 @@ let process_class sec_sp ids_to_discard x =
           let newsp = Lib.make_path spid CCI in 
 	  let hyps = (Global.lookup_mind sp).mind_hyps in
 	  let n = count_extra_abstractions hyps ids_to_discard in
-(*
-          let v = global_reference CCI spid in
-          let t = Retyping.get_type_of env Evd.empty v in
-          let p = arity_sort t in
-*)
           (CL_IND (newsp,i),{cl_strength=stre;cl_param=p+n})
         else 
 	  x
diff --git a/toplevel/command.ml b/toplevel/command.ml
index b93cc8b6a..51af38e20 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -308,7 +308,7 @@ let build_recursive lnameargsardef =
   let lrefrec = Array.mapi declare namerec in
   if_verbose pPNL (recursive_message lrefrec);
   (* The others are declared as normal definitions *)
-  let var_subst id = (id, global_reference CCI id) in
+  let var_subst id = (id, global_reference id) in
   let _ = 
     List.fold_left
       (fun subst (f,def) ->
@@ -370,7 +370,7 @@ let build_corecursive lnameardef =
   in 
   let lrefrec = Array.mapi declare namerec in
   if_verbose pPNL (corecursive_message lrefrec);
-  let var_subst id = (id, global_reference CCI id) in
+  let var_subst id = (id, global_reference id) in
   let _ = 
     List.fold_left
       (fun subst (f,def) ->
@@ -385,17 +385,12 @@ let build_corecursive lnameardef =
   in
   ()
 
-let inductive_of_ident id =
-  let c =
-    try global_reference CCI id
-    with Not_found ->
-      errorlabstrm "inductive_of_ident"
-	[< 'sTR ((string_of_id id) ^ " not found") >]
-  in
-  match kind_of_term (global_reference CCI id) with
-    | IsMutInd ind -> ind
-    | _ -> errorlabstrm "inductive_of_ident"
-	[< 'sTR (string_of_id id); 'sPC; 'sTR "is not an inductive type" >]
+let inductive_of_ident qid =
+  match Nametab.global dummy_loc qid with
+    | IndRef ind -> ind
+    | ref -> errorlabstrm "inductive_of_ident"
+	[< 'sTR (Global.string_of_global ref); 
+           'sPC; 'sTR "is not an inductive type">]
 
 let build_scheme lnamedepindsort = 
   let lrecnames = List.map (fun (f,_,_,_) -> f) lnamedepindsort
diff --git a/toplevel/command.mli b/toplevel/command.mli
index 63456e33b..f45dc633f 100644
--- a/toplevel/command.mli
+++ b/toplevel/command.mli
@@ -49,7 +49,7 @@ val build_recursive :
 
 val build_corecursive :  (identifier * Coqast.t * Coqast.t) list -> unit
 
-val build_scheme : (identifier * bool * identifier * Coqast.t) list -> unit
+val build_scheme : (identifier * bool * Nametab.qualid * Coqast.t) list -> unit
 
 val start_proof_com : identifier option -> strength -> Coqast.t -> unit
 
diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml
index 9b634bf08..01b868aa2 100644
--- a/toplevel/discharge.ml
+++ b/toplevel/discharge.ml
@@ -314,16 +314,12 @@ let close_section _ s =
   let newdir = dirpath sec_sp in
   let olddir = wd_of_sp sec_sp in
   let (ops,ids,_) = 
-    if Options.immediate_discharge then ([],[],([],[],[]))
-    else
-      List.fold_left 
-	(process_item oldenv newdir olddir) ([],[],([],[],[])) decls 
+    List.fold_left 
+      (process_item oldenv newdir olddir) ([],[],([],[],[])) decls 
   in
   let ids = last_section_hyps olddir in
   Global.pop_named_decls ids;
   Summary.unfreeze_lost_summaries fs;
   add_frozen_state ();
-  if Options.immediate_discharge then ()
-  else
-    catch_not_found (List.iter process_operation) (List.rev ops);
+  catch_not_found (List.iter process_operation) (List.rev ops);
   Nametab.push_section olddir
diff --git a/toplevel/record.ml b/toplevel/record.ml
index 87cb11b61..a8f90e3ec 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -87,7 +87,7 @@ let declare_projections indsp coers fields =
   let paramdecls = 
     List.map (fun (na,b,t) -> match na with Name id -> (id,b,t) | _ -> assert false)
       paramdecls in
-  let r = constr_of_reference Evd.empty (Global.env()) (IndRef indsp) in
+  let r = mkMutInd indsp in
   let paramargs = List.rev (List.map (fun (id,_,_) -> mkVar id) paramdecls) in
   let rp = applist (r, paramargs) in
   let x = Environ.named_hd (Global.env()) r Anonymous in
@@ -117,7 +117,6 @@ let declare_projections indsp coers fields =
 	     it_mkNamedLambda_or_LetIn (mkLambda (x, rp, body)) paramdecls in
 	   let name = 
 	     try
-	       let proj = instantiate_inductive_section_params proj indsp in
 	       let cie = { const_entry_body = proj;
                            const_entry_type = None;
                            const_entry_opaque = false } in
@@ -132,8 +131,7 @@ let declare_projections indsp coers fields =
 	     | None -> (None::sp_projs, fi::ids_not_ok, subst)
 	     | Some sp ->
 		 let refi = ConstRef sp in
-		 let constr_fi =
-		   constr_of_reference Evd.empty (Global.env()) refi in
+		 let constr_fi = mkConst sp in
 		 if coe then begin
 		   let cl = Class.class_of_ref (IndRef indsp) in
 		   Class.try_add_new_coercion_with_source 
diff --git a/toplevel/recordobj.ml b/toplevel/recordobj.ml
index ac4642722..dac63126a 100755
--- a/toplevel/recordobj.ml
+++ b/toplevel/recordobj.ml
@@ -45,7 +45,7 @@ let trait t =
 let objdef_declare ref =
   let sp = match ref with ConstRef sp -> sp | _ -> objdef_err ref in
   let env = Global.env () in
-  let v = constr_of_reference Evd.empty env ref in
+  let v = constr_of_reference ref in
   let vc =
     match kind_of_term v with
       | IsConst cst ->
@@ -82,6 +82,6 @@ let objdef_declare ref =
         List.iter 
 	  (fun (spi,(ci,l_ui)) -> 
 	     add_new_objdef 
-	       ((ConstRef spi,cte_of_constr ci),v,lt,params,l_ui)) comp
+	       ((ConstRef spi,reference_of_constr ci),v,lt,params,l_ui)) comp
     | _ -> objdef_err ref
                  
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index bdf448afe..d4d51073d 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -106,21 +106,6 @@ let show_top_evars () =
   let sigma = project gls in 
   mSG (pr_evars_int 1 (Evd.non_instantiated sigma))
 
-(* Locate commands *)
-let locate_qualid loc qid =
-  try Nametab.locate qid
-  with Not_found -> 
-  try
-    let _ = Syntax_def.locate_syntactic_definition qid in
-    error
-      ("Unexpected reference to a syntactic definition: "
-       ^(Nametab.string_of_qualid qid))
-  with Not_found ->
-    Nametab.error_global_not_found_loc loc qid
-
- (* Pour pcoq *)
-let global = locate_qualid
-
 let locate_file f =
   try
     let _,file =
@@ -514,7 +499,7 @@ let _ =
        | _  -> bad_vernac_args "IMPLICIT_ARGS_OFF")
 
 let coercion_of_qualid loc qid =
-  let ref = locate_qualid loc qid in
+  let ref = Nametab.global loc qid in
   let coe = Classops.coe_of_reference ref in
   if not (Classops.coercion_exists coe) then
     errorlabstrm "try_add_coercion" 
@@ -537,10 +522,10 @@ let _ =
 	   (fun () ->
 	      let imps = number_list l in
 	      Impargs.declare_manual_implicits
-		(locate_qualid dummy_loc qid) imps)
+		(Nametab.global dummy_loc qid) imps)
        | [VARG_STRING "Auto"; VARG_QUALID qid] -> 
 	   (fun () -> 
-	      Impargs.declare_implicits (locate_qualid dummy_loc qid))
+	      Impargs.declare_implicits (Nametab.global dummy_loc qid))
        | _  -> bad_vernac_args "IMPLICITS")
 
 let interp_definition_kind = function
@@ -597,7 +582,7 @@ let _ =
        List.iter 
 	 (function 
 	    | VARG_QUALID qid ->
-                (match locate_qualid dummy_loc qid with
+                (match Nametab.global dummy_loc qid with
                   | ConstRef sp -> Opaque.set_transparent_const sp
                   | VarRef sp -> Opaque.set_transparent_var (basename sp) 
                   | _ -> error
@@ -611,7 +596,7 @@ let _ =
        List.iter
 	 (function 
 	    | VARG_QUALID qid ->
-                (match locate_qualid dummy_loc qid with
+                (match Nametab.global dummy_loc qid with
                   | ConstRef sp -> Opaque.set_opaque_const sp
                   | VarRef sp -> Opaque.set_opaque_var (basename sp) 
                   | _ -> error
@@ -1024,7 +1009,7 @@ let _ =
     (function 
        | (VARG_QUALID qid) :: l ->
 	   (fun () ->
-	      let ref = locate_qualid dummy_loc qid in
+	      let ref = Nametab.global dummy_loc qid in
 	      Search.search_by_head ref (inside_outside l))
        | _ -> bad_vernac_args "SEARCH")
 
@@ -1221,7 +1206,7 @@ let _ =
 		  | (VARG_VARGLIST 
 		       [VARG_IDENTIFIER fid;
 			VARG_STRING depstr;
-			VARG_IDENTIFIER indid;
+			VARG_QUALID indid;
 			VARG_CONSTR sort]) ->
 		      let dep = match depstr with 
 			| "DEP" -> true
@@ -1296,7 +1281,7 @@ let _ =
 	       NeverDischarge 
 	   in
 	   fun () -> 
-	     let ref = locate_qualid dummy_loc qid in
+	     let ref = Nametab.global dummy_loc qid in
 	     Class.try_add_new_class ref stre;
              if_verbose message
                ((Nametab.string_of_qualid qid) ^ " is now a class")
@@ -1306,7 +1291,7 @@ let cl_of_qualid qid =
   match Nametab.repr_qualid qid with
     | [], id when string_of_id id = "FUNCLASS" -> Classops.CL_FUN
     | [], id when string_of_id id = "SORTCLASS" -> Classops.CL_SORT
-    | _ -> Class.class_of_ref (locate_qualid dummy_loc qid)	
+    | _ -> Class.class_of_ref (Nametab.global dummy_loc qid)	
 
 let _ =
   add "COERCION"
@@ -1328,7 +1313,7 @@ let _ =
 		   Class.try_add_new_identity_coercion id stre source target
 	       | _ -> bad_vernac_args "COERCION"
 	     else
-	       let ref = locate_qualid dummy_loc qid in
+	       let ref = Nametab.global dummy_loc qid in
 	       Class.try_add_new_coercion_with_target ref stre source target;
 	       if_verbose
 		 message
@@ -1356,8 +1341,10 @@ let _ =
 let _ =
   add "PrintPATH"
     (function 
-       | [VARG_IDENTIFIER ids;VARG_IDENTIFIER idt] -> 
-	   (fun () -> pPNL (Prettyp.print_path_between ids idt))
+       | [VARG_QUALID qids;VARG_QUALID qidt] -> 
+	   (fun () ->
+              pPNL (Prettyp.print_path_between
+                      (cl_of_qualid qids) (cl_of_qualid qidt)))
        | _ -> bad_vernac_args "PrintPATH")
 
 (* Meta-syntax commands *)
@@ -1509,7 +1496,7 @@ let _ =
 	      let key = 
 		SecondaryTable (string_of_id t,string_of_id f) in
 	      try 
-		(get_ident_table key)#add (locate_qualid dummy_loc v)
+		(get_ident_table key)#add (Nametab.global dummy_loc v)
 	      with Not_found -> 
 		error_undeclared_key key)
        | [VARG_IDENTIFIER t; VARG_IDENTIFIER f; VARG_STRING s] -> 
@@ -1524,7 +1511,7 @@ let _ =
 	   (fun () ->
 	      let key = PrimaryTable (string_of_id t) in
 	      try 
-		(get_ident_table key)#add (locate_qualid dummy_loc v)
+		(get_ident_table key)#add (Nametab.global dummy_loc v)
 	      with Not_found -> 
 		error_undeclared_key key)
        | [VARG_IDENTIFIER t; VARG_STRING s] ->
@@ -1558,7 +1545,7 @@ let _ =
 	      let key = 
 		SecondaryTable (string_of_id t,string_of_id f) in
 	      try 
-		(get_ident_table key)#remove (locate_qualid dummy_loc v)
+		(get_ident_table key)#remove (Nametab.global dummy_loc v)
 	      with Not_found -> 
 		error_undeclared_key key)
        | [VARG_IDENTIFIER t; VARG_IDENTIFIER f; VARG_STRING v] -> 
@@ -1573,7 +1560,7 @@ let _ =
 	   (fun () ->
 	      let key = PrimaryTable (string_of_id t) in
 	      try 
-		(get_ident_table key)#remove (locate_qualid dummy_loc v)
+		(get_ident_table key)#remove (Nametab.global dummy_loc v)
 	      with Not_found -> 
 		error_undeclared_key key)
        | [VARG_IDENTIFIER t; VARG_STRING v] -> 
@@ -1614,7 +1601,7 @@ let _ =
 	      let key = 
 		SecondaryTable (string_of_id t,string_of_id f) in
 	      try 
-		(get_ident_table key)#mem (locate_qualid dummy_loc v)
+		(get_ident_table key)#mem (Nametab.global dummy_loc v)
 	      with Not_found -> 
 		error_undeclared_key key)
        | [VARG_IDENTIFIER t; VARG_IDENTIFIER f; VARG_STRING v] -> 
@@ -1629,7 +1616,7 @@ let _ =
 	   (fun () ->
 	      let key = PrimaryTable (string_of_id t) in
 	      try 
-		(get_ident_table key)#mem (locate_qualid dummy_loc v)
+		(get_ident_table key)#mem (Nametab.global dummy_loc v)
 	      with Not_found -> 
 		error_undeclared_key key)
        | [VARG_IDENTIFIER t; VARG_IDENTIFIER v] -> 
diff --git a/toplevel/vernacentries.mli b/toplevel/vernacentries.mli
index 6c829e5a2..5aa37beeb 100644
--- a/toplevel/vernacentries.mli
+++ b/toplevel/vernacentries.mli
@@ -30,11 +30,6 @@ val show_node : unit -> unit
    in the context of the current goal, as for instance in pcoq *)
 val get_current_context_of_args : vernac_arg list -> Proof_type.enamed_declarations * Environ.env
 
-(* This function is used to transform a qualified identifier into a
-   global reference, with a nice error message in case of failure.
-   It is used in pcoq. *)
-val global : Coqast.loc -> Nametab.qualid -> global_reference;;
-
 (* this function is used to analyse the extra arguments in search commands.
    It is used in pcoq. *)
 val inside_outside : vernac_arg list -> dir_path list * bool;;