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

7 files changed, 231 insertions, 166 deletions

diff --git a/toplevel/class.ml b/toplevel/class.ml
index 37ef4eb92..587caae76 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 f8aada5f5..fd1ee3f8f 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 c4119ccbf..02f1635e9 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 c0479acf6..3b20efe07 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 45f50d441..91d65a5f9 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 d6093fdc1..ac2c6836e 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 5714bbded..e17490ddb 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 _ =