Prise en compte des noms longs dans les Hints et les Coercions, et réorganisations diverses

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

14 files changed, 300 insertions, 248 deletions

diff --git a/library/declare.ml b/library/declare.ml
index 3fd30327e7..ead0fa6b15 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -78,7 +78,8 @@ let (in_variable, out_variable) =
 
 let declare_variable id obj =
   let sp = add_leaf id CCI (in_variable (id,obj)) in
-  if is_implicit_args() then declare_var_implicits sp
+  if is_implicit_args() then declare_var_implicits sp;
+  sp
 
 (* Parameters. *)
 
@@ -106,7 +107,8 @@ let (in_parameter, out_parameter) =
 
 let declare_parameter id c =
   let sp = add_leaf id CCI (in_parameter c) in 
-  if is_implicit_args() then declare_constant_implicits sp
+  if is_implicit_args() then declare_constant_implicits sp;
+  sp
 
 (* Constants. *)
 
@@ -165,8 +167,9 @@ let hcons_constant_declaration = function
 let declare_constant id cd =
   (* let cd = hcons_constant_declaration cd in *)
   let sp = add_leaf id CCI (in_constant cd) in
-  if is_implicit_args() then declare_constant_implicits sp
- 
+  if is_implicit_args() then declare_constant_implicits sp;
+  sp
+
 (* Inductives. *)
 
 
@@ -376,7 +379,7 @@ let construct_reference env kind id =
   with Not_found ->
     mkVar (let _ = Environ.lookup_named id env in id)
 
-let global_qualified_reference qid = 
+let global_qualified_reference qid =
   construct_qualified_reference (Global.env()) qid
 
 let global_absolute_reference sp = 
@@ -385,11 +388,6 @@ let global_absolute_reference sp =
 let global_reference kind id = 
   construct_reference (Global.env()) kind id
 
-(*
-let global env id =
-  try let _ = lookup_glob id (Environ.context env) in mkVar id
-  with Not_found -> global_reference CCI id
-*)
 let dirpath_of_global = function
   | EvarRef n -> ["evar"]
   | VarRef sp -> dirpath sp
@@ -430,9 +428,9 @@ let elimination_suffix = function
 let declare_one_elimination mispec =
   let mindstr = string_of_id (mis_typename mispec) in
   let declare na c =
-    declare_constant (id_of_string na)
+    let _ = declare_constant (id_of_string na)
       (ConstantEntry { const_entry_body = c; const_entry_type = None }, 
-       NeverDischarge,false);
+       NeverDischarge,false) in
     if Options.is_verbose() then pPNL [< 'sTR na; 'sTR " is defined" >]
   in
   let env = Global.env () in
@@ -445,33 +443,7 @@ let declare_one_elimination mispec =
     (fun (sort,suff) -> 
        if List.mem sort kelim then declare (mindstr^suff) (make_elim sort))
     eliminations
-(*
-let declare_eliminations sp i =
-  let mib = Global.lookup_mind sp in
 
-  if not (list_subset ids (ids_of_named_context (Global.named_context ()))) then
-    error ("Declarations of elimination scheme outside the section "^
-    "of the inductive definition is not implemented");
-  let ctxt = instance_from_named_context mib.mind_hyps in
-  let mispec = Global.lookup_mind_specif ((sp,i),Array.of_list ctxt) in 
-  let mindstr = string_of_id (mis_typename mispec) in
-  let declare na c =
-    declare_constant (id_of_string na)
-      (ConstantEntry { const_entry_body = c; const_entry_type = None }, 
-       NeverDischarge,false);
-    if Options.is_verbose() then pPNL [< 'sTR na; 'sTR " is defined" >]
-  in
-  let env = Global.env () in
-  let sigma = Evd.empty in
-  let elim_scheme = build_indrec env sigma mispec in
-  let npars = mis_nparams mispec in
-  let make_elim s = instanciate_indrec_scheme s npars elim_scheme in
-  let kelim = mis_kelim mispec in
-  List.iter
-    (fun (sort,suff) -> 
-       if List.mem sort kelim then declare (mindstr^suff) (make_elim sort))
-    eliminations
-*)
 let declare_eliminations sp =
   let mib = Global.lookup_mind sp in
   let ids = ids_of_named_context mib.mind_hyps in
diff --git a/library/declare.mli b/library/declare.mli
index 927f05fde1..e561f222e0 100644
--- a/library/declare.mli
+++ b/library/declare.mli
@@ -29,7 +29,7 @@ type sticky = bool
 
 type variable_declaration = section_variable_entry * strength * sticky
 
-val declare_variable : identifier -> variable_declaration -> unit
+val declare_variable : identifier -> variable_declaration -> variable_path
 
 type constant_declaration_type =
   | ConstantEntry  of constant_entry
@@ -39,10 +39,16 @@ type opacity = bool
 
 type constant_declaration = constant_declaration_type * strength * opacity
 
-val declare_constant : identifier -> constant_declaration -> unit
+(* [declare_constant id cd] declares a global declaration
+   (constant/parameter) with name [id] in the current section; it returns
+   the full path of the declaration *)
+val declare_constant : identifier -> constant_declaration -> constant_path
 
-val declare_parameter : identifier -> constr -> unit
+val declare_parameter : identifier -> constr -> constant_path
 
+(* [declare_constant id cd] declares a block of inductive types with
+   their constructors in the current section; it returns the path of
+   the whole block *)
 val declare_mind : mutual_inductive_entry -> section_path
 
 (* [declare_eliminations sp] declares elimination schemes associated
diff --git a/pretyping/pattern.mli b/pretyping/pattern.mli
index 5c5c28ba1b..d69b5e7242 100644
--- a/pretyping/pattern.mli
+++ b/pretyping/pattern.mli
@@ -30,6 +30,8 @@ type constr_label =
   | VarNode of identifier
   | SectionVarNode of section_path
 
+val label_of_ref : global_reference -> constr_label
+
 exception BoundPattern
 
 (* [head_pattern_bound t] extracts the head variable/constant of the
diff --git a/tactics/auto.ml b/tactics/auto.ml
index 89b16ea8a9..3825da2eff 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -34,7 +34,7 @@ type auto_tactic =
   | ERes_pf    of constr * unit clausenv (* Hint EApply *)
   | Give_exact of constr                  
   | Res_pf_THEN_trivial_fail of constr * unit clausenv (* Hint Immediate *)
-  | Unfold_nth of constr                 (* Hint Unfold *)
+  | Unfold_nth of global_reference       (* Hint Unfold *)
   | Extern of Coqast.t                   (* Hint Extern *) 
 
 type pri_auto_tactic = { 
@@ -265,20 +265,17 @@ let add_resolves env sigma clist dbnames =
 	    )))
     dbnames
 
-(* REM : in most cases hintname = id *)
+let global qid =
+  try Nametab.locate qid
+  with Not_found -> Pretype_errors.error_global_not_found_loc dummy_loc qid
 
-let make_unfold (hintname, id) =
-  let hdconstr = 
-    (try 
-       Declare.global_reference CCI id
-     with Not_found -> 
-       errorlabstrm  "make_unfold" [<pr_id id; 'sTR " not declared" >])
-  in 
-  (head_of_constr_reference hdconstr, 
+(* REM : in most cases hintname = id *)
+let make_unfold (hintname, ref) =
+  (Pattern.label_of_ref ref,
    { hname = hintname;
      pri = 4;
      pat = None;
-     code = Unfold_nth hdconstr })
+     code = Unfold_nth ref })
 
 let add_unfolds l dbnames =
   List.iter 
@@ -329,11 +326,14 @@ let _ =
   vinterp_add
     "HintUnfold"
     (function 
-       | [ VARG_IDENTIFIER hintname; VARG_VARGLIST l; VARG_IDENTIFIER id] ->
+       | [ VARG_IDENTIFIER hintname; VARG_VARGLIST l; VARG_QUALID qid] ->
 	   let dbnames = if l = [] then ["core"] else 
-	     List.map (function VARG_IDENTIFIER i -> string_of_id i
-		      	 | _ -> bad_vernac_args "HintUnfold") l in
-      	   fun () -> add_unfolds [(hintname, id)] dbnames
+	     List.map
+	       (function VARG_IDENTIFIER i -> string_of_id i
+		  | _ -> bad_vernac_args "HintUnfold") l in
+      	   fun () -> 
+	     let ref = global qid in
+	     add_unfolds [(hintname, ref)] dbnames
        | _-> bad_vernac_args "HintUnfold")
     
 let _ = 
@@ -365,22 +365,22 @@ let _ =
   vinterp_add
     "HintConstructors"
     (function 
-       | [VARG_IDENTIFIER idr; VARG_VARGLIST l; VARG_IDENTIFIER c] ->
+       | [VARG_IDENTIFIER idr; VARG_VARGLIST l; VARG_QUALID qid] ->
 	   begin 
 	     try
 	       let env = Global.env() and sigma = Evd.empty in
-	       let trad = Declare.global_reference CCI in
-	       let rectype = destMutInd (trad c) in
+	       let rectype = destMutInd (Declare.global_qualified_reference qid) in
 	       let consnames = 
 		 mis_consnames (Global.lookup_mind_specif rectype) in
 	       let lcons = 
-		 array_map_to_list (fun id -> (id, trad id)) consnames in
+		 array_map_to_list
+		   (fun id -> (id, Declare.global_reference CCI id)) consnames in
 	       let dbnames = if l = [] then ["core"] else 
 	      	 List.map (function VARG_IDENTIFIER i -> string_of_id i
 			     | _ -> bad_vernac_args "HintConstructors") l in
     	       fun () -> add_resolves env sigma lcons dbnames
 	     with Invalid_argument("mind_specif_of_mind") -> 
-	       error ((string_of_id c) ^ " is not an inductive type")
+	       error ((string_of_qualid qid) ^ " is not an inductive type")
 	   end 
        | _ -> bad_vernac_args "HintConstructors")
     
@@ -405,10 +405,18 @@ let _ =
        | (VARG_VARGLIST l)::lh ->
 	   let env = Global.env() and sigma = Evd.empty in
  	   let lhints = 
-	     List.map (function
-			 | VARG_IDENTIFIER i -> 
-			     (i, Declare.global_reference CCI i)
-		      	 | _-> bad_vernac_args "HintsResolve") lh in
+	     List.map
+	       (function
+		  | VARG_QUALID qid -> 
+		      let c =
+			try Declare.global_qualified_reference qid
+		        with Not_found -> 
+			  errorlabstrm "global_reference"
+			    [<'sTR ("Cannot find reference "
+				    ^(string_of_qualid qid))>] in
+		      let _,i = repr_qualid qid in
+		      (id_of_string 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
 		      	 | _-> bad_vernac_args "HintsResolve") l in
@@ -422,7 +430,9 @@ let _ =
        | (VARG_VARGLIST l)::lh ->
 	   let lhints = 
 	     List.map (function
-			 | VARG_IDENTIFIER i -> (i, i)
+			 | VARG_QUALID qid ->
+			     let _,n = repr_qualid qid in
+			     (id_of_string n, global qid)
 		      	 | _ -> bad_vernac_args "HintsUnfold") lh in
 	   let dbnames = if l = [] then ["core"] else 
 	     List.map (function 
@@ -438,8 +448,10 @@ let _ =
        | (VARG_VARGLIST l)::lh ->
 	   let lhints = 
 	     List.map (function
-			 | VARG_IDENTIFIER i -> 
-			     (i, Declare.global_reference CCI i)
+			 | VARG_QUALID qid -> 
+			     let _,n = repr_qualid qid in
+			     (id_of_string n,
+			      Declare.global_qualified_reference qid)
 		      	 | _ -> bad_vernac_args "HintsImmediate") lh in
 	   let dbnames = if l = [] then ["core"] else 
 	     List.map (function 
@@ -458,7 +470,7 @@ let fmt_autotactic = function
   | Give_exact c -> [< 'sTR"Exact " ; prterm c >]
   | Res_pf_THEN_trivial_fail (c,clenv) -> 
       [< 'sTR"Apply "; prterm c ; 'sTR" ; Trivial" >]
-  | Unfold_nth c -> [< 'sTR"Unfold " ;  prterm c >]
+  | Unfold_nth c -> [< 'sTR"Unfold " ;  pr_global c >]
   | Extern coqast -> [< 'sTR "Extern "; gentacpr coqast >]
 
 let fmt_hint_list hintlist =
diff --git a/tactics/auto.mli b/tactics/auto.mli
index 24c426d31b..6a7e9d3e96 100644
--- a/tactics/auto.mli
+++ b/tactics/auto.mli
@@ -19,7 +19,7 @@ type auto_tactic =
   | ERes_pf    of constr * unit clausenv    (* Hint EApply *)
   | Give_exact of constr                  
   | Res_pf_THEN_trivial_fail of constr * unit clausenv (* Hint Immediate *)
-  | Unfold_nth of constr                    (* Hint Unfold *)
+  | Unfold_nth of global_reference          (* Hint Unfold *)
   | Extern     of Coqast.t (* Hint Extern *)
 
 open Rawterm
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 087821d7ab..1080b95092 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -221,15 +221,10 @@ let dyn_reduce = function
 
 (* Unfolding occurrences of a constant *)
 
-let unfold_constr c = 
-  match kind_of_term (strip_outer_cast c) with 
-    | IsConst(sp,_) -> 
-	unfold_in_concl [[],sp]
-    | IsVar(id) -> let sp = Lib.make_path id CCI in
-	unfold_in_concl [[],sp]
-    | _ -> 
-	errorlabstrm "unfold_constr"
-	  [< 'sTR "Cannot unfold a non-constant." >]
+let unfold_constr = function 
+  | ConstRef sp -> unfold_in_concl [[],sp]
+  | VarRef sp -> unfold_in_concl [[],sp]
+  | _ -> errorlabstrm "unfold_constr" [< 'sTR "Cannot unfold a non-constant.">]
 
 (*******************************************)
 (*         Introduction tactics            *)
@@ -1718,9 +1713,9 @@ let abstract_subproof name tac gls =
       with e when catchable_exception e -> 
 	(delete_current_proof(); raise e)
     in   (* Faudrait un peu fonctionnaliser cela *)
-    Declare.declare_constant na (ConstantEntry const,strength,true);
+    let sp = Declare.declare_constant na (ConstantEntry const,strength,true) in
     let newenv = Global.env() in
-    Declare.construct_reference newenv CCI na
+    Declare.constr_of_reference Evd.empty newenv (ConstRef sp)
   in
   exact_no_check (applist (lemme,
 		  List.map mkVar (List.rev (ids_of_named_context sign))))
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 4c1bc9770a..9caeafde6e 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -125,7 +125,7 @@ val reduce            : red_expr -> identifier list -> tactic
 val dyn_reduce        : tactic_arg list -> tactic
 val dyn_change        : tactic_arg list -> tactic
 
-val unfold_constr     : constr -> tactic
+val unfold_constr     : global_reference -> tactic
 val pattern_option    : 
   (int list * constr * constr) list -> identifier option -> tactic
 
diff --git a/toplevel/class.ml b/toplevel/class.ml
index 37ef4eb925..587caae76e 100644
--- a/toplevel/class.ml
+++ b/toplevel/class.ml
@@ -91,8 +91,8 @@ let try_add_class v (cl,p) streopt check_exist =
 
 (* try_add_new_class : Names.identifier -> unit *)
 
-let try_add_new_class id stre =
-  let v = global_reference CCI id in
+let try_add_new_class ref stre =
+  let v = constr_of_reference Evd.empty (Global.env()) ref in
   let env = Global.env () in
   let t = Retyping.get_type_of env Evd.empty v in
   let p1 =
@@ -100,7 +100,7 @@ let try_add_new_class id stre =
       arity_sort t 
     with Not_found -> 
       errorlabstrm "try_add_class" 
-        [< 'sTR "Type of "; 'sTR (string_of_id id);
+        [< 'sTR "Type of "; Printer.pr_global ref;
            'sTR " does not end with a sort" >] 
   in
   let cl = fst (constructor_at_head v) in
@@ -109,7 +109,7 @@ let try_add_new_class id stre =
 (* check_class : Names.identifier ->
   Term.constr -> cl_typ -> int -> int * Libobject.strength *)
 
-let check_class id v cl p =
+let check_class v cl p =
   try 
     let _,clinfo = class_info cl in
     check_fully_applied cl p clinfo.cL_PARAM;
@@ -121,13 +121,23 @@ let check_class id v cl p =
       try 
 	arity_sort t 
       with Not_found -> 
-	errorlabstrm "try_add_class" 
-          [< 'sTR "Type of "; 'sTR (string_of_id id);
+	errorlabstrm "check_class" 
+          [< 'sTR "Type of "; 'sTR (string_of_class cl);
              'sTR " does not end with a sort" >] 
     in
     check_fully_applied cl p p1;
     try_add_class v (cl,p1) None false
 
+(* check that the computed target is the provided one *)
+let check_target clt = function
+    | None -> ()
+    | Some cl -> 
+	if cl <> clt then 
+	  errorlabstrm "try_add_coercion" 
+            [<'sTR"Found target class "; 'sTR(string_of_class cl);
+	      'sTR " while "; 'sTR(string_of_class clt);
+	      'sTR " is expected" >]
+
 (* decomposition de constr vers coe_typ *)
 
 (* t provient de global_reference donc pas de Cast, pas de App *)
@@ -177,7 +187,18 @@ let id_of_cl  = function
   | CL_IND (sp,i) ->
       (mind_nth_type_packet (Global.lookup_mind sp) i).mind_typename
   | CL_SECVAR sp -> (basename sp)
-	
+
+let class_of_ref = function
+  | ConstRef sp -> CL_CONST sp
+  | IndRef sp -> CL_IND sp
+  | VarRef sp -> CL_SECVAR sp
+  | ConstructRef _ as c -> 
+      errorlabstrm "class_of_ref"
+	[< 'sTR "Constructors, such as "; Printer.pr_global c; 
+	   'sTR " cannot be used as class" >]
+  | EvarRef _ -> 
+      errorlabstrm "class_of_ref"
+	[< 'sTR "Existential variables cannot be used as class" >]
 (* 
 lp est la liste (inverse'e) des arguments de la coercion
 ids est le nom de la classe source
@@ -193,24 +214,24 @@ la liste des variables dont depend la classe source
 let get_source lp source =
   match source with
     | None ->
-	let (v1,lv1,l,cl1,p1) as x =
+	let (v1,lv1,l,cl1,p1) =
 	  match lp with
 	    | [] -> raise Not_found
             | t1::_ ->
 		try constructor_at_head1 t1
                 with _ -> raise Not_found
         in 
-	(id_of_cl cl1),(cl1,p1,v1,lv1,1,l)
-    | Some id -> 
+	(cl1,p1,v1,lv1,1,l)
+    | Some cl ->
 	let rec aux n = function
 	  | [] -> raise Not_found
 	  | t1::lt ->
 	      try 
 		let v1,lv1,l,cl1,p1 = constructor_at_head1 t1 in
-		if id_of_cl cl1 = id then cl1,p1,v1,lv1,n,l
+		if cl1 = cl then cl1,p1,v1,lv1,n,l
 		else aux (n+1) lt
               with _ -> aux (n + 1) lt
-	in id, aux 1 lp
+	in aux 1 lp
 
 let get_target t ind =
   if (ind > 1) then 
@@ -226,23 +247,20 @@ let prods_of t =
   in 
   aux [] t
 
-(* coercion identite' *)
+(* coercion identité *)
 
-let build_id_coercion idf_opt ids =
+let error_not_transparent source =
+  errorlabstrm "build_id_coercion"
+    [< 'sTR ((string_of_class source)^" must be a transparent constant") >]
+
+let build_id_coercion idf_opt source =
   let env = Global.env () in
-  let vs = construct_reference env CCI ids in 
-  let c = match kind_of_term (strip_outer_cast vs) with
-    | IsConst cst -> 
-	(try Instantiate.constant_value env cst
-         with Instantiate.NotEvaluableConst _ ->
-	   errorlabstrm "build_id_coercion"
-             [< 'sTR(string_of_id ids);
-		'sTR" must be a transparent constant" >])
-    | _ -> 
-	errorlabstrm "build_id_coercion"
-          [< 'sTR(string_of_id ids); 
-	     'sTR" must be a transparent constant" >] 
-  in
+  let vs = match source with
+    | CL_CONST sp -> constr_of_reference Evd.empty env (ConstRef sp)
+    | _ -> error_not_transparent source in
+  let c = match Instantiate.constant_opt_value env (destConst vs) with
+    | Some c -> c
+    | None -> error_not_transparent source in
   let lams,t = Sign.decompose_lam_assum c in
   let llams = List.length lams in
   let lams = List.rev lams in
@@ -269,19 +287,19 @@ let build_id_coercion idf_opt ids =
   in
   let idf =
     match idf_opt with
-      | Some(idf) -> idf
+      | Some idf -> idf
       | None ->
-	  id_of_string ("Id_"^(string_of_id ids)^"_"^
+	  id_of_string ("Id_"^(string_of_class source)^"_"^
                         (string_of_class (fst (constructor_at_head t)))) 
   in
   let constr_entry = (* Cast is necessary to express [val_f] is identity *)
+    ConstantEntry
+      { const_entry_body = mkCast (val_f, typ_f);
+	const_entry_type = None } in
+  let sp = declare_constant idf (constr_entry,NeverDischarge,false) in
+  ConstRef sp
 
-    { const_entry_body = mkCast (val_f, typ_f);
-      const_entry_type = None } in
-  declare_constant idf (ConstantEntry constr_entry,NeverDischarge,false);
-  idf
-
-let add_new_coercion_in_graph1 (coef,v,stre,isid,cls,clt) idf ps =
+let add_new_coercion_in_graph1 (coef,v,stre,isid,cls,clt) ps =
   add_anonymous_leaf
     (inCoercion
        ((coef,
@@ -301,18 +319,18 @@ lorque source est None alors target est None aussi.
 
 let try_add_new_coercion_core idf stre source target isid =
   let env = Global.env () in
-  let v = construct_reference env CCI idf in
+  let v = constr_of_reference Evd.empty env idf in
   let vj = Retyping.get_judgment_of env Evd.empty v in
   let f_vardep,coef = coe_of_reference v in
   if coercion_exists coef then
     errorlabstrm "try_add_coercion" 
-      [< 'sTR(string_of_id idf) ; 'sTR" is already a coercion" >];
+      [< Printer.pr_global idf; 'sTR" is already a coercion" >];
   let lp = prods_of (vj.uj_type) in
   let llp = List.length lp in
   if llp <= 1 then
     errorlabstrm "try_add_coercion"         
       [< 'sTR"Does not correspond to a coercion" >];
-  let ids,(cls,ps,vs,lvs,ind,s_vardep) =
+  let (cls,ps,vs,lvs,ind,s_vardep) =
     try 
       get_source (List.tl lp) source
     with Not_found -> 
@@ -327,8 +345,8 @@ let try_add_new_coercion_core idf stre source target isid =
       [< 'sTR"SORTCLASS cannot be a source class" >];
   if not (uniform_cond (llp-1-ind) lvs) then
     errorlabstrm "try_add_coercion" 
-      [<'sTR(string_of_id idf);
-        'sTR" does not respect the inheritance uniform condition" >];
+      [< Printer.pr_global idf;
+         'sTR" does not respect the inheritance uniform condition" >];
   let clt,pt,vt =
     try 
       get_target (List.hd lp) ind 
@@ -336,19 +354,9 @@ let try_add_new_coercion_core idf stre source target isid =
       errorlabstrm "try_add_coercion" 
         [<'sTR"We cannot find the target class" >] 
   in
-  let idt =
-    (match target with
-       | Some idt -> 
-	   if idt = id_of_cl clt then 
-	     idt
-	   else 
-	     errorlabstrm "try_add_coercion" 
-               [<'sTR"The target class does not correspond to ";
-		 'sTR(string_of_id idt) >]
-       | None -> (id_of_cl clt)) 
-  in
-  let stres = check_class ids vs cls ps in
-  let stret = check_class idt vt clt pt in
+  check_target clt target;
+  let stres = check_class vs cls ps in
+  let stret = check_class vt clt pt in
   let stref = stre_of_coe coef in
 (* 01/00: Supprimé la prise en compte de la force des variables locales. Sens ?
   let streunif = stre_unif_cond (s_vardep,f_vardep) in
@@ -357,29 +365,29 @@ let try_add_new_coercion_core idf stre source target isid =
   let stre' = stre_max4 stres stret stref streunif in
   (* if (stre=NeverDischarge) & (stre'<>NeverDischarge)
      then errorlabstrm "try_add_coercion" 
-     [<'sTR(string_of_id idf);
+     [< pr_global idf;
      'sTR" must be declared as a local coercion (its strength is ";
      'sTR(string_of_strength stre');'sTR")" >] *)
   let stre = stre_max (stre,stre') in
-  add_new_coercion_in_graph1 (coef,vj,stre,isid,cls,clt) idf ps
+  add_new_coercion_in_graph1 (coef,vj,stre,isid,cls,clt) ps
 
 
-let try_add_new_coercion id stre =
-  try_add_new_coercion_core id stre None None false
+let try_add_new_coercion ref stre =
+  try_add_new_coercion_core ref stre None None false
 
-let try_add_new_coercion_subclass id stre =
-  let idf = build_id_coercion None id in
-  try_add_new_coercion_core idf stre (Some id) None true
+let try_add_new_coercion_subclass cl stre =
+  let coe_ref = build_id_coercion None cl in
+  try_add_new_coercion_core coe_ref stre (Some cl) None true
 
-let try_add_new_coercion_with_target id stre source target isid =
-  if isid then
-    let idf = build_id_coercion (Some id) source in
-    try_add_new_coercion_core idf stre (Some source) (Some target) true
-  else 
-    try_add_new_coercion_core id stre (Some source) (Some target) false
+let try_add_new_coercion_with_target ref stre source target =
+  try_add_new_coercion_core ref stre (Some source) (Some target) false
+
+let try_add_new_identity_coercion id stre source target =
+  let ref = build_id_coercion (Some id) source in
+  try_add_new_coercion_core ref stre (Some source) (Some target) true
 
-let try_add_new_coercion_record id stre source =
-  try_add_new_coercion_core id stre (Some source) None false
+let try_add_new_coercion_with_source ref stre source =
+  try_add_new_coercion_core ref stre (Some source) None false
 
 (* fonctions pour le discharge: plutot sale *)
 
diff --git a/toplevel/class.mli b/toplevel/class.mli
index f8aada5f56..fd1ee3f8f5 100644
--- a/toplevel/class.mli
+++ b/toplevel/class.mli
@@ -10,16 +10,42 @@ open Declare
 
 (* Classes and coercions. *)
 
-val try_add_new_coercion : identifier -> strength -> unit
-val try_add_new_coercion_subclass : identifier -> strength -> unit
-val try_add_new_coercion_record : identifier -> strength -> identifier -> unit
-val try_add_new_coercion_with_target : identifier -> strength ->
-  identifier -> identifier -> bool -> unit
+(* [try_add_new_coercion_with_target ref s src tg] declares [ref] as a coercion
+   from [src] to [tg] *)
+val try_add_new_coercion_with_target : global_reference -> strength -> 
+  source:cl_typ -> target:cl_typ ->  unit
 
-val try_add_new_class : identifier -> strength -> unit
+(* [try_add_new_coercion ref s] declares [ref], assumed to be of type
+   [(x1:T1)...(xn:Tn)src->tg], as a coercion from [src] to [tg] *)
+val try_add_new_coercion : global_reference -> strength -> unit
+
+(* [try_add_new_coercion_subclass cst s] expects that [cst] denotes a
+   transparent constant which unfolds to some class [tg]; it declares
+   an identity coercion from [cst] to [tg], named something like
+   ["Id_cst_tg"] *)
+val try_add_new_coercion_subclass : cl_typ -> strength -> unit
+
+(* [try_add_new_coercion_with_source ref s src] declares [ref] as a coercion
+   from [src] to [tg] where the target is inferred from the type of [ref] *)
+val try_add_new_coercion_with_source : global_reference -> strength ->
+  source:cl_typ -> unit
+
+(* [try_add_new_identity_coercion id s src tg] enriches the
+   environment with a new definition of name [id] declared as an
+   identity coercion from [src] to [tg] *)
+val try_add_new_identity_coercion : identifier -> strength ->
+  source:cl_typ -> target:cl_typ -> unit
+
+(* [try_add_new_class ref] declares [ref] as a new class; usually,
+   this is done implicitely by try_add_new_coercion's functions *)
+val try_add_new_class : global_reference -> strength -> unit
+
+(*s This is used for the discharge *)
 val process_class :
   dir_path -> identifier list -> 
     (cl_typ * cl_info_typ) -> (cl_typ * cl_info_typ)
 val process_coercion :
   dir_path -> (coe_typ * coe_info_typ) * cl_typ * cl_typ -> 
     (coe_typ * coe_info_typ) * cl_typ * cl_typ
+
+val class_of_ref : global_reference -> cl_typ
diff --git a/toplevel/command.ml b/toplevel/command.ml
index c4119ccbfb..02f1635e93 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -57,11 +57,12 @@ let constr_of_constr_entry ce =
     | Some t -> mkCast (ce.const_entry_body, t)
 
 let declare_global_definition ident ce n local =
-  declare_constant ident (ConstantEntry ce,n,false);
+  let sp = declare_constant ident (ConstantEntry ce,n,false) in
   if local then
     wARNING [< pr_id ident; 'sTR" is declared as a global definition" >];
   if is_verbose() then
-    message ((string_of_id ident) ^ " is defined")
+    message ((string_of_id ident) ^ " is defined");
+  ConstRef sp
 
 let definition_body_red red_option ident (local,n) com comtypeopt = 
   let ce = constant_entry_of_com (com,comtypeopt) in
@@ -71,11 +72,12 @@ let definition_body_red red_option ident (local,n) com comtypeopt =
     | DischargeAt disch_sp ->
         if Lib.is_section_p disch_sp then begin
 	  let c = constr_of_constr_entry ce' in
-          declare_variable ident (SectionLocalDef c,n,false);
+          let sp = declare_variable ident (SectionLocalDef c,n,false) in
 	  if is_verbose() then message ((string_of_id ident) ^ " is defined");
           if Pfedit.refining () then 
             mSGERRNL [< 'sTR"Warning: Local definition "; pr_id ident; 
-                        'sTR" is not visible from current goals" >]
+                        'sTR" is not visible from current goals" >];
+	  VarRef sp
         end
 	else
 	  declare_global_definition ident ce' n true
@@ -95,13 +97,15 @@ let syntax_definition ident com =
 
 let parameter_def_var ident c =
   let c = interp_type Evd.empty (Global.env()) c in
-  declare_parameter (id_of_string ident) c;
-  if is_verbose() then message (ident ^ " is assumed")
+  let sp = declare_parameter (id_of_string ident) c in
+  if is_verbose() then message (ident ^ " is assumed");
+  sp
 
 let declare_global_assumption ident c =
-  parameter_def_var ident c;
+  let sp = parameter_def_var ident c in
   wARNING [< 'sTR ident; 'sTR" is declared as a parameter";
-             'sTR" because it is at a global level" >]
+             'sTR" because it is at a global level" >];
+  ConstRef sp
 
 let hypothesis_def_var is_refining ident n c =
   match n with
@@ -109,12 +113,13 @@ let hypothesis_def_var is_refining ident n c =
     | DischargeAt disch_sp ->
         if Lib.is_section_p disch_sp then begin
 	  let t = interp_type Evd.empty (Global.env()) c in
-          declare_variable (id_of_string ident)
-             (SectionLocalAssum t,n,false);
+          let sp = declare_variable (id_of_string ident)
+		     (SectionLocalAssum t,n,false) in
 	  if is_verbose() then message (ident ^ " is assumed");
           if is_refining then 
             mSGERRNL [< 'sTR"Warning: Variable "; 'sTR ident; 
-                        'sTR" is not visible from current goals" >]
+                        'sTR" is not visible from current goals" >];
+	  VarRef sp
         end
 	else
 	  declare_global_assumption ident c
@@ -132,14 +137,14 @@ let minductive_message = function
 
 let recursive_message = function 
   | []  -> anomaly "no recursive definition"
-  | [x] -> [< pr_id x; 'sTR " is recursively defined">]
-  | l   -> hOV 0 [< prlist_with_sep pr_coma pr_id l;
+  | [sp] -> [< Printer.pr_global sp; 'sTR " is recursively defined">]
+  | l   -> hOV 0 [< prlist_with_sep pr_coma Printer.pr_global l;
 		    'sPC; 'sTR "are recursively defined">]
 
 let corecursive_message = function 
   | []  -> anomaly "no corecursive definition"
-  | [x] -> [< pr_id x; 'sTR " is corecursively defined">]
-  | l   -> hOV 0 [< prlist_with_sep pr_coma pr_id l;
+  | [x] -> [< Printer.pr_global x; 'sTR " is corecursively defined">]
+  | l   -> hOV 0 [< prlist_with_sep pr_coma Printer.pr_global l;
                     'sPC; 'sTR "are corecursively defined">]
 
 let interp_mutual lparams lnamearconstrs finite = 
@@ -250,8 +255,8 @@ let build_recursive lnameargsardef =
         (fun (env,arl) (recname,lparams,arityc,_) -> 
            let raw_arity = mkProdCit lparams arityc in
            let arity = interp_type sigma env0 raw_arity in
-           declare_variable recname
-	     (SectionLocalAssum arity, NeverDischarge, false);
+           let _ = declare_variable recname
+	     (SectionLocalAssum arity, NeverDischarge, false) in
            (Environ.push_named_assum (recname,arity) env, (arity::arl)))
         (env0,[]) lnameargsardef
     with e ->
@@ -284,13 +289,13 @@ let build_recursive lnameargsardef =
 			recvec));
 	      const_entry_type = None } 
 	  in
-	  declare_constant fi (ConstantEntry ce, n, false);
-          declare (i+1) lf
-      | _ -> () 
+	  let sp = declare_constant fi (ConstantEntry ce, n, false) in
+          (ConstRef sp)::(declare (i+1) lf)
+      | _ -> [] 
     in 
     (* declare the recursive definitions *)
-    declare 0 lnamerec; 
-    if is_verbose() then pPNL(recursive_message lnamerec)
+    let lrefrec = declare 0 lnamerec in
+    if is_verbose() then pPNL(recursive_message lrefrec)
   end;
   (* The others are declared as normal definitions *)
   let var_subst id = (id, global_reference CCI id) in
@@ -299,7 +304,7 @@ let build_recursive lnameargsardef =
       (fun subst (f,def) ->
 	 let ce = { const_entry_body = replace_vars subst def;
 		    const_entry_type = None } in
-	 declare_constant f (ConstantEntry ce,n,false);
+	 let _ = declare_constant f (ConstantEntry ce,n,false) in
       	 warning ((string_of_id f)^" is non-recursively defined");
       	 (var_subst f) :: subst)
       (List.map var_subst lnamerec)
@@ -318,8 +323,8 @@ let build_corecursive lnameardef =
         (fun (env,arl) (recname,arityc,_) -> 
            let arj = type_judgment_of_rawconstr Evd.empty env0 arityc in
 	   let arity = arj.utj_val in
-           declare_variable recname
-	     (SectionLocalAssum arj.utj_val,NeverDischarge,false);
+           let _ = declare_variable recname
+	     (SectionLocalAssum arj.utj_val,NeverDischarge,false) in
            (Environ.push_named_assum (recname,arity) env, (arity::arl)))
         (env0,[]) lnameardef
     with e -> 
@@ -353,12 +358,12 @@ let build_corecursive lnameardef =
 			     recvec));
 	      const_entry_type = None } 
 	  in
-          declare_constant fi (ConstantEntry ce,n,false);
-          declare (i+1) lf
-      | _        -> () 
+          let sp = declare_constant fi (ConstantEntry ce,n,false) in
+          (ConstRef sp) :: declare (i+1) lf
+      | _        -> [] 
     in 
-    declare 0 lnamerec; 
-    if is_verbose() then pPNL(corecursive_message lnamerec)
+    let lrefrec = declare 0 lnamerec in
+    if is_verbose() then pPNL(corecursive_message lrefrec)
   end;
   let var_subst id = (id, global_reference CCI id) in
   let _ = 
@@ -366,7 +371,7 @@ let build_corecursive lnameardef =
       (fun subst (f,def) ->
 	 let ce = { const_entry_body = replace_vars subst def;
 		    const_entry_type = None } in
-	 declare_constant f (ConstantEntry ce,n,false);
+	 let _ = declare_constant f (ConstantEntry ce,n,false) in
       	 warning ((string_of_id f)^" is non-recursively defined");
       	 (var_subst f) :: subst)
       (List.map var_subst lnamerec)
@@ -397,12 +402,13 @@ let build_scheme lnamedepindsort =
   in
   let n = NeverDischarge in 
   let listdecl = Indrec.build_mutual_indrec env0 sigma lrecspec in 
-  let rec declare decl fi =
-    let ce = { const_entry_body = decl; const_entry_type = None } 
-    in declare_constant fi (ConstantEntry ce,n,false)
+  let rec declare decl fi lrecref =
+    let ce = { const_entry_body = decl; const_entry_type = None } in
+    let sp = declare_constant fi (ConstantEntry ce,n,false) in
+    ConstRef sp :: lrecref
   in 
-  List.iter2 declare listdecl lrecnames; 
-  if is_verbose() then pPNL(recursive_message lrecnames)
+  let lrecref = List.fold_right2 declare listdecl lrecnames [] in
+  if is_verbose() then pPNL(recursive_message lrecref)
 
 let start_proof_com sopt stre com =
   let env = Global.env () in
@@ -428,9 +434,9 @@ let save opacity id ({const_entry_body = pft; const_entry_type = tpo} as const)
   begin match strength with
     | DischargeAt disch_sp when Lib.is_section_p disch_sp ->
 	let c = constr_of_constr_entry const in
-	declare_variable id (SectionLocalDef c,strength,opacity)
+	let _ = declare_variable id (SectionLocalDef c,strength,opacity) in ()
     | NeverDischarge | DischargeAt _ ->
-        declare_constant id (ConstantEntry const,strength,opacity)
+        let _ = declare_constant id (ConstantEntry const,strength,opacity)in ()
     | NotDeclare -> apply_tac_not_declare id pft tpo
   end;
   if not (strength = NotDeclare) then
diff --git a/toplevel/command.mli b/toplevel/command.mli
index c0479acf6c..3b20efe071 100644
--- a/toplevel/command.mli
+++ b/toplevel/command.mli
@@ -7,14 +7,16 @@ open Term
 open Declare
 (*i*)
 
-(* Declaration functions. The following functions take ASTs, transform them
-   into [constr] and then call the corresponding functions of [Declare]. *)
+(*s Declaration functions. The following functions take ASTs,
+   transform them into [constr] and then call the corresponding
+   functions of [Declare]; they return an absolute reference to the
+   defined object *)
 
 val definition_body : identifier -> bool * strength -> 
-  Coqast.t -> Coqast.t option -> unit
+  Coqast.t -> Coqast.t option -> global_reference
 
-val definition_body_red : Tacred.red_expr option ->  
-  identifier -> bool * strength -> Coqast.t -> Coqast.t option -> unit
+val definition_body_red : Tacred.red_expr option -> identifier
+  -> bool * strength -> Coqast.t -> Coqast.t option -> global_reference
 
 val syntax_definition : identifier -> Coqast.t -> unit
 
@@ -22,9 +24,10 @@ val syntax_definition : identifier -> Coqast.t -> unit
 val abstraction_definition : identifier -> int array -> Coqast.t -> unit
 i*)
 
-val hypothesis_def_var : bool -> string -> strength -> Coqast.t -> unit
+val hypothesis_def_var : bool -> string -> strength -> Coqast.t
+  -> global_reference
 
-val parameter_def_var : string -> Coqast.t -> unit
+val parameter_def_var : string -> Coqast.t -> constant_path
 
 val build_mutual : 
   (identifier * Coqast.t) list -> 
diff --git a/toplevel/record.ml b/toplevel/record.ml
index 45f50d4419..91d65a5f95 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -77,8 +77,8 @@ let warning_or_error coe err =
   pPNL (hOV 0 [< 'sTR"Warning: "; st >])
 
 (* We build projections *)
-let declare_projections idstruc coers paramdecls fields =
-  let r = global_reference CCI idstruc in
+let declare_projections structref coers paramdecls fields =
+  let r = constr_of_reference Evd.empty (Global.env()) structref 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
@@ -105,25 +105,29 @@ let declare_projections idstruc coers paramdecls fields =
 		 mkMutCase (ci, p, mkRel 1, [|branch|]) in
 	   let proj =
 	     it_mkNamedLambda_or_LetIn (mkLambda (x, rp, body)) paramdecls in
-	   let ok = 
+	   let name = 
 	     try
 	       let cie = { const_entry_body = proj; const_entry_type = None} in
-	       declare_constant fi (ConstantEntry cie,NeverDischarge,false); 
-	       true
+	       let sp =
+		 declare_constant fi (ConstantEntry cie,NeverDischarge,false)
+	       in Some sp
              with Type_errors.TypeError (k,ctx,te) -> begin
                warning_or_error coe (BadTypedProj (fi,k,ctx,te));
-	       false
+	       None
 	     end in
-	   if not ok then 
-	     (None::sp_projs,fi::ids_not_ok,subst)
-	   else begin
-             if coe then
-	       Class.try_add_new_coercion_record fi NeverDischarge idstruc;
-             let constr_fi = global_reference CCI fi in
-             let constr_fip = applist (constr_fi,proj_args)
-             in (Some(path_of_const constr_fi)::sp_projs,
-		 ids_not_ok, (fi,constr_fip)::subst)
-	   end)
+	   match name with
+	     | 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
+		 if coe then begin
+		   let cl = Class.class_of_ref structref in
+		   Class.try_add_new_coercion_with_source 
+		     refi NeverDischarge cl
+		 end;
+		 let constr_fip = applist (constr_fi,proj_args) in
+		 (name::sp_projs, ids_not_ok, (fi,constr_fip)::subst))
       ([],[],[]) coers (List.rev fields)
   in sp_projs
 
@@ -164,7 +168,8 @@ let definition_structure (is_coe,idstruc,ps,cfs,idbuild,s) =
     { mind_entry_finite = true;
       mind_entry_inds = [mie_ind] } in
   let sp = declare_mutual_with_eliminations mie in
-  let sp_projs = declare_projections idstruc coers params fields in
-  let rsp = (sp,0) in
-  if is_coe then Class.try_add_new_coercion idbuild NeverDischarge;
+  let rsp = (sp,0) in (* This is ind path of idstruc *)
+  let sp_projs = declare_projections (IndRef rsp) coers params fields in
+  let build = ConstructRef (rsp,1) in (* This is construct path of idbuild *)
+  if is_coe then Class.try_add_new_coercion build NeverDischarge;
   Recordops.add_new_struc (rsp,idbuild,nparams,List.rev sp_projs)
diff --git a/toplevel/record.mli b/toplevel/record.mli
index d6093fdc11..ac2c6836ed 100644
--- a/toplevel/record.mli
+++ b/toplevel/record.mli
@@ -7,13 +7,13 @@ open Term
 open Sign
 (*i*)
 
-(* [declare_projections id coers params fields] declare projections of
-   record [id] (if allowed), and put them as coercions accordingly to
-   [coers] *)
+(* [declare_projections ref coers params fields] declare projections of
+   record [ref] (if allowed), and put them as coercions accordingly to
+   [coers]; it returns the absolute names of projections *)
 
 val declare_projections :
-  identifier -> bool list -> 
-   named_context -> named_context -> constant_path option list
+  global_reference -> bool list -> 
+    named_context -> named_context -> constant_path option list
 
 val definition_structure :
    bool * identifier * (identifier * Coqast.t) list *
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 5714bbded3..e17490ddbd 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -105,7 +105,10 @@ let show_top_evars () =
   mSG (pr_evars_int 1 (Evd.non_instantiated sigma))
 
 (* Locate commands *)
- 
+let global loc qid =
+  try Nametab.locate qid
+  with Not_found -> Pretype_errors.error_global_not_found_loc loc qid
+
 let locate_file f =
   try
     let _,file = System.where_in_path (get_load_path()) f in
@@ -829,7 +832,7 @@ let _ =
                            'sPC; 'sTR "failed";
                            'sTR "... converting to Axiom" >];
                   delete_proof s;
-                  parameter_def_var (string_of_id s) com
+                  let _ = parameter_def_var (string_of_id s) com in ()
            	end else 
 		  errorlabstrm "Vernacentries.TheoremProof"
                     [< 'sTR "checking of theorem "; pr_id s; 'sPC;
@@ -864,14 +867,16 @@ let _ =
              | _       -> anomaly "Unexpected string"
 	   in 
 	   fun () ->
-	     definition_body_red red_option id (local,stre) c typ_opt;
+	     let ref =
+	       definition_body_red red_option id (local,stre) c typ_opt in
              if coe then begin
-	       Class.try_add_new_coercion id stre;
+	       Class.try_add_new_coercion ref stre;
                if not (is_silent()) then
 		 message ((string_of_id id) ^ " is now a coercion")
 	     end;
-	     if idcoe then 
-	       Class.try_add_new_coercion_subclass id stre;
+	     if idcoe then
+	       let cl = Class.class_of_ref ref in
+	       Class.try_add_new_coercion_subclass cl stre;
              (***TODO if objdef then Recordobj.objdef_declare id ***)
        | _ -> bad_vernac_args "DEFINITION")
 
@@ -896,10 +901,11 @@ let _ =
 	       (fun (sl,c) -> 
 		  List.iter 
 		    (fun s ->
-                       hypothesis_def_var (refining()) (string_of_id s) 
-			 stre c;
+                       let ref = 
+			 hypothesis_def_var 
+			   (refining()) (string_of_id s) stre c in
                        if coe then
-			 Class.try_add_new_coercion s stre)
+			 Class.try_add_new_coercion ref stre)
                     sl)
 	       slcl
        | _ -> bad_vernac_args "VARIABLE")
@@ -915,7 +921,7 @@ let _ =
 	       (fun (sl,c) ->
 		  List.iter 
 		    (fun s -> 
-		       parameter_def_var (string_of_id s) c)
+		       let _ = parameter_def_var (string_of_id s) c in ())
 		    sl)
                slcl
        | _ -> bad_vernac_args "PARAMETER")
@@ -991,12 +997,7 @@ let _ =
     (function 
        | (VARG_QUALID qid) :: l ->
 	   (fun () ->
-	      let ref =
-		try 
-		  Nametab.locate qid
-		with Not_found ->
-		  Pretype_errors.error_global_not_found_loc loc qid
-	      in 
+	      let ref = global dummy_loc qid in
 	      Search.search_by_head ref (inside_outside l))
        | _ -> bad_vernac_args "SEARCH")
 
@@ -1277,7 +1278,7 @@ let _ =
 let _ =
   add "CLASS"
     (function 
-       | [VARG_STRING kind;VARG_IDENTIFIER id] -> 
+       | [VARG_STRING kind; VARG_QUALID qid] -> 
 	   let stre = 
 	     if kind = "LOCAL" then 
 	       make_strength_0()
@@ -1285,16 +1286,23 @@ let _ =
 	       NeverDischarge 
 	   in
 	   fun () -> 
-	     Class.try_add_new_class id stre;
+	     let ref = global dummy_loc qid in
+	     Class.try_add_new_class ref stre;
              if not (is_silent()) then
-               message ((string_of_id id) ^ " is now a class")
+               message ((string_of_qualid qid) ^ " is now a class")
        | _ -> bad_vernac_args "CLASS")
 
+let cl_of_qualid qid =
+  match repr_qualid qid with
+    | [], "FUNCLASS" -> Classops.CL_FUN
+    | [], "SORTCLASS" -> Classops.CL_SORT
+    | _ -> Class.class_of_ref (global dummy_loc qid)	
+
 let _ =
   add "COERCION"
     (function 
        | [VARG_STRING kind;VARG_STRING identity;
-          VARG_IDENTIFIER id;VARG_IDENTIFIER ids;VARG_IDENTIFIER idt] -> 
+          VARG_QUALID qid;VARG_QUALID qids;VARG_QUALID qidt] -> 
 	   let stre = 
 	     if (kind = "LOCAL") then 
 	       make_strength_0()
@@ -1302,10 +1310,19 @@ let _ =
 	       NeverDischarge 
 	   in
 	   let isid = identity = "IDENTITY" in
-	   fun () -> 
-	     Class.try_add_new_coercion_with_target id stre ids idt isid;
+	   let target = cl_of_qualid qidt in
+	   let source = cl_of_qualid qids in
+	   fun () ->
+	     if isid then match repr_qualid qid with
+	       | [], s ->
+		   let id = id_of_string s in
+		   Class.try_add_new_identity_coercion id stre source target
+	       | _ -> bad_vernac_args "COERCION"
+	     else
+	       let ref = global dummy_loc qid in
+	       Class.try_add_new_coercion_with_target ref stre source target;
              if not (is_silent()) then
-	       message ((string_of_id id) ^ " is now a coercion")
+	       message ((string_of_qualid qid) ^ " is now a coercion")
        | _ -> bad_vernac_args "COERCION")
 
 let _ =