Added a Local Definition vernacular command. This type of definition

has to be refered through its qualified name even when the module
containing it is imported.

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

10 files changed, 189 insertions, 150 deletions

diff --git a/toplevel/autoinstance.ml b/toplevel/autoinstance.ml
index 3eb77bc06..97d655da5 100644
--- a/toplevel/autoinstance.ml
+++ b/toplevel/autoinstance.ml
@@ -184,8 +184,8 @@ let declare_record_instance gr ctx params =
 	     const_entry_type=None;
          const_entry_opaque=false;
          const_entry_inline_code = false } in
-  let cst = Declare.declare_constant ident
-    (DefinitionEntry ce,Decl_kinds.IsDefinition Decl_kinds.StructureComponent) in
+  let decl = (DefinitionEntry ce,Decl_kinds.IsDefinition Decl_kinds.StructureComponent) in
+  let cst = Declare.declare_constant ident decl in
   new_instance_message ident (Typeops.type_of_constant (Global.env()) cst) def
 
 let declare_class_instance gr ctx params =
diff --git a/toplevel/class.ml b/toplevel/class.ml
index 9d93d39f6..8f8f70816 100644
--- a/toplevel/class.ml
+++ b/toplevel/class.ml
@@ -20,7 +20,9 @@ open Globnames
 open Nametab
 open Decl_kinds
 
-let strength_min l = if List.mem Local l then Local else Global
+let strength_min l = if List.mem `LOCAL l then `LOCAL else `GLOBAL
+
+let loc_of_bool b = if b then `LOCAL else `GLOBAL
 
 (* Errors *)
 
@@ -147,13 +149,13 @@ let prods_of t =
   aux [] t
 
 let strength_of_cl = function
-  | CL_CONST kn -> Global
-  | CL_SECVAR id -> Local
-  | _ -> Global
+  | CL_CONST kn -> `GLOBAL
+  | CL_SECVAR id -> `LOCAL
+  | _ -> `GLOBAL
 
 let strength_of_global = function
-  | VarRef _ -> Local
-  | _ -> Global
+  | VarRef _ -> `LOCAL
+  | _ -> `GLOBAL
 
 let get_strength stre ref cls clt =
   let stres = strength_of_cl cls in
@@ -220,7 +222,8 @@ let build_id_coercion idf_opt source =
         const_entry_opaque = false;
 	const_entry_inline_code = true
       } in
-  let kn = declare_constant idf (constr_entry,IsDefinition IdentityCoercion) in
+  let decl = (constr_entry, IsDefinition IdentityCoercion) in
+  let kn = declare_constant idf decl in
   ConstRef kn
 
 let check_source = function
@@ -263,37 +266,50 @@ let add_new_coercion_core coef stre source target isid =
   check_target clt target;
   check_arity cls;
   check_arity clt;
-  let stre' = get_strength stre coef cls clt in
-  declare_coercion coef stre' ~isid ~src:cls ~target:clt ~params:(List.length lvs)
+  let local = match get_strength stre coef cls clt with
+  | `LOCAL -> true
+  | `GLOBAL -> false
+  in
+  declare_coercion coef ~local ~isid ~src:cls ~target:clt ~params:(List.length lvs)
 
-let try_add_new_coercion_core ref b c d e =
-  try add_new_coercion_core ref b c d e
+let try_add_new_coercion_core ref ~local c d e =
+  try add_new_coercion_core ref (loc_of_bool local) c d e
   with CoercionError e ->
       errorlabstrm "try_add_new_coercion_core"
         (explain_coercion_error ref e ++ str ".")
 
-let try_add_new_coercion ref stre =
-  try_add_new_coercion_core ref stre None None false
+let try_add_new_coercion ref ~local =
+  try_add_new_coercion_core ref ~local None None false
 
-let try_add_new_coercion_subclass cl stre =
+let try_add_new_coercion_subclass cl ~local =
   let coe_ref = build_id_coercion None cl in
-  try_add_new_coercion_core coe_ref stre (Some cl) None true
+  try_add_new_coercion_core coe_ref ~local (Some cl) None true
 
-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_coercion_with_target ref ~local ~source ~target =
+  try_add_new_coercion_core ref ~local (Some source) (Some target) false
 
-let try_add_new_identity_coercion id stre ~source ~target =
+let try_add_new_identity_coercion id ~local ~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_with_source ref stre ~source =
-  try_add_new_coercion_core ref stre (Some source) None false
+  try_add_new_coercion_core ref ~local (Some source) (Some target) true
 
-let add_coercion_hook stre ref =
-  try_add_new_coercion ref stre;
-  Flags.if_verbose msg_info
-    (pr_global_env Id.Set.empty ref ++ str " is now a coercion")
+let try_add_new_coercion_with_source ref ~local ~source =
+  try_add_new_coercion_core ref ~local (Some source) None false
 
-let add_subclass_hook stre ref =
+let add_coercion_hook local ref =
+  let stre = match local with
+  | Local -> true
+  | Global -> false
+  | Discharge -> assert false
+  in
+  let () = try_add_new_coercion ref stre in
+  let msg = pr_global_env Id.Set.empty ref ++ str " is now a coercion" in
+  Flags.if_verbose msg_info msg
+
+let add_subclass_hook local ref =
+  let stre = match local with
+  | Local -> true
+  | Global -> false
+  | Discharge -> assert false
+  in
   let cl = class_of_global ref in
   try_add_new_coercion_subclass cl stre
diff --git a/toplevel/class.mli b/toplevel/class.mli
index a72ec1a81..0d39ee170 100644
--- a/toplevel/class.mli
+++ b/toplevel/class.mli
@@ -18,28 +18,28 @@ open Nametab
 
 (** [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 -> locality ->
+val try_add_new_coercion_with_target : global_reference -> local:bool ->
   source:cl_typ -> target:cl_typ ->  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 -> locality -> unit
+val try_add_new_coercion : global_reference -> local:bool -> 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 -> locality -> unit
+val try_add_new_coercion_subclass : cl_typ -> local:bool -> 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 -> locality ->
+val try_add_new_coercion_with_source : global_reference -> local:bool ->
   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 : Id.t -> locality ->
+val try_add_new_identity_coercion : Id.t -> local:bool ->
   source:cl_typ -> target:cl_typ -> unit
 
 val add_coercion_hook : unit Tacexpr.declaration_hook
diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index 03fc6bd1f..570e66deb 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -99,16 +99,15 @@ let instance_hook k pri global imps ?hook cst =
   (match hook with Some h -> h cst | None -> ())
 
 let declare_instance_constant k pri global imps ?hook id term termtype =
-  let cdecl =
-    let kind = IsDefinition Instance in
-    let entry =
-      { const_entry_body   = term;
-        const_entry_secctx = None;
-	const_entry_type   = Some termtype;
-	const_entry_opaque = false;
-	const_entry_inline_code = false }
-    in DefinitionEntry entry, kind
+  let kind = IsDefinition Instance in
+  let entry = {
+    const_entry_body   = term;
+    const_entry_secctx = None;
+    const_entry_type   = Some termtype;
+    const_entry_opaque = false;
+    const_entry_inline_code = false }
   in
+  let cdecl = (DefinitionEntry entry, kind) in
   let kn = Declare.declare_constant id cdecl in
     Declare.definition_message id;
     instance_hook k pri global imps ?hook (ConstRef kn);
@@ -321,27 +320,27 @@ let context l =
   let _, ((env', fullctx), impls) = interp_context_evars evars env l in
   let fullctx = Evarutil.nf_rel_context_evar !evars fullctx in
   let ce t = Evarutil.check_evars env Evd.empty !evars t in
-  List.iter (fun (n, b, t) -> Option.iter ce b; ce t) fullctx;
+  let () = List.iter (fun (n, b, t) -> Option.iter ce b; ce t) fullctx in
   let ctx = try named_of_rel_context fullctx with _ ->
     error "Anonymous variables not allowed in contexts."
   in
   let fn status (id, _, t) =
     if Lib.is_modtype () && not (Lib.sections_are_opened ()) then
-      let cst = Declare.declare_constant ~internal:Declare.KernelSilent id
-	(ParameterEntry (None,t,None), IsAssumption Logical)
-      in
+      let decl = (ParameterEntry (None,t,None), IsAssumption Logical) in
+      let cst = Declare.declare_constant ~internal:Declare.KernelSilent id decl in
 	match class_of_constr t with
 	| Some (rels, (tc, args) as _cl) ->
 	    add_instance (Typeclasses.new_instance tc None false (ConstRef cst));
             status
 	    (* declare_subclasses (ConstRef cst) cl *)
 	| None -> status
-    else (
-      let impl = List.exists 
-	(fun (x,_) ->
-	   match x with ExplByPos (_, Some id') -> Id.equal id id' | _ -> false) impls
+    else
+      let test (x, _) = match x with
+      | ExplByPos (_, Some id') -> Id.equal id id'
+      | _ -> false
       in
-	Command.declare_assumption false (Local (* global *), Definitional) t
-	  [] impl (* implicit *) None (* inline *) (Loc.ghost, id) && status)
+      let impl = List.exists test impls in
+      let decl = (Discharge, Definitional) in
+      let nstatus = Command.declare_assumption false decl t [] impl None (Loc.ghost, id) in
+      status && nstatus
   in List.fold_left fn true (List.rev ctx)
-       
diff --git a/toplevel/command.ml b/toplevel/command.ml
index d5a1da6d0..21bb963db 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -112,35 +112,43 @@ let check_definition (ce, evd, imps) =
     Option.iter (check_evars env Evd.empty evd) ce.const_entry_type;
     ce
 
+let get_locality id = function
+| Discharge ->
+  (** If a Let is defined outside a section, then we consider it as a local definition *)
+  let msg = pr_id id ++ strbrk " is declared as a local definition" in
+  let () = if Flags.is_verbose () then msg_warning msg in
+  true
+| Local -> true
+| Global -> false
+
 let declare_global_definition ident ce local k imps =
-  let kn = declare_constant ident (DefinitionEntry ce,IsDefinition k) in
+  let local = get_locality ident local in
+  let kn = declare_constant ident ~local (DefinitionEntry ce, IsDefinition k) in
   let gr = ConstRef kn in
-    maybe_declare_manual_implicits false gr imps;
-    if local == Local && Flags.is_verbose() then
-      msg_warning (pr_id ident ++ strbrk " is declared as a global definition");
-    definition_message ident;
-    Autoinstance.search_declaration (ConstRef kn);
-    gr
+  let () = maybe_declare_manual_implicits false gr imps in
+  let () = definition_message ident in
+  let () = Autoinstance.search_declaration (ConstRef kn) in
+  gr
 
 let declare_definition_hook = ref ignore
 let set_declare_definition_hook = (:=) declare_definition_hook
 let get_declare_definition_hook () = !declare_definition_hook
 
-let declare_definition ident (local,k) ce imps hook =
-  !declare_definition_hook ce;
+let declare_definition ident (local, k) ce imps hook =
+  let () = !declare_definition_hook ce in
   let r = match local with
-    | Local when Lib.sections_are_opened () ->
-        let c =
-          SectionLocalDef(ce.const_entry_body ,ce.const_entry_type,false) in
-        let _ = declare_variable ident (Lib.cwd(),c,IsDefinition k) in
-        definition_message ident;
-        if Pfedit.refining () then
-          Flags.if_warn msg_warning
-	    (strbrk "Local definition " ++ pr_id ident ++
-             strbrk " is not visible from current goals");
-        VarRef ident
-    | (Global|Local) ->
-        declare_global_definition ident ce local k imps in
+  | Discharge when Lib.sections_are_opened () ->
+    let c = SectionLocalDef(ce.const_entry_body, ce.const_entry_type, false) in
+    let _ = declare_variable ident (Lib.cwd(), c, IsDefinition k) in
+    let () = definition_message ident in
+    let () = if Pfedit.refining () then
+      let msg = strbrk "Section definition " ++
+        pr_id ident ++ strbrk " is not visible from current goals" in
+      Flags.if_warn msg_warning msg
+    in
+    VarRef ident
+  | Discharge | Local | Global ->
+    declare_global_definition ident ce local k imps in
   hook local r
 
 let _ = Obligations.declare_definition_ref := declare_definition
@@ -158,40 +166,37 @@ let do_definition ident k bl red_option c ctypopt hook =
       let obls, _, c, cty = 
 	Obligations.eterm_obligations env ident evd 0 c typ
       in
-	ignore(Obligations.add_definition ident ~term:c cty ~implicits:imps ~kind:k ~hook obls)
+      ignore(Obligations.add_definition ident ~term:c cty ~implicits:imps ~kind:k ~hook obls)
     else let ce = check_definition def in
       declare_definition ident k ce imps hook
 
 (* 2| Variable/Hypothesis/Parameter/Axiom declarations *)
 
-let declare_assumption is_coe (local,kind) c imps impl nl (_,ident) =
-  let r,status = match local with
-    | Local when Lib.sections_are_opened () ->
-        let _ =
-          declare_variable ident
-            (Lib.cwd(), SectionLocalAssum (c,impl), IsAssumption kind) in
-        assumption_message ident;
-        if is_verbose () && Pfedit.refining () then
-          msg_warning (str"Variable" ++ spc () ++ pr_id ident ++
-          strbrk " is not visible from current goals");
-	let r = VarRef ident in
-	  Typeclasses.declare_instance None true r; r,true
-    | (Global|Local) ->
-        let kn =
-          declare_constant ident 
-            (ParameterEntry (None,c,nl), IsAssumption kind) in
-	let gr = ConstRef kn in
-	  maybe_declare_manual_implicits false gr imps;
-        assumption_message ident;
-        if local == Local && Flags.is_verbose () then
-          msg_warning (pr_id ident ++ strbrk " is declared as a parameter" ++
-          strbrk " because it is at a global level");
-	Autoinstance.search_declaration (ConstRef kn);
-	Typeclasses.declare_instance None false gr;
-        gr , (Lib.is_modtype_strict ())
+let declare_assumption is_coe (local,kind) c imps impl nl (_,ident) = match local with
+| Discharge when Lib.sections_are_opened () ->
+  let decl = (Lib.cwd(), SectionLocalAssum (c,impl), IsAssumption kind) in
+  let _ = declare_variable ident decl in
+  let () = assumption_message ident in
+  let () =
+    if is_verbose () && Pfedit.refining () then
+    msg_warning (str"Variable" ++ spc () ++ pr_id ident ++
+    strbrk " is not visible from current goals")
   in
-    if is_coe then Class.try_add_new_coercion r local;
-    status
+  let r = VarRef ident in
+  let () = Typeclasses.declare_instance None true r in
+  let () = if is_coe then Class.try_add_new_coercion r ~local:true in
+  true
+| Global | Local | Discharge ->
+  let local = get_locality ident local in
+  let decl = (ParameterEntry (None,c,nl), IsAssumption kind) in
+  let kn = declare_constant ident ~local decl in
+  let gr = ConstRef kn in
+  let () = maybe_declare_manual_implicits false gr imps in
+  let () = assumption_message ident in
+  let () = Autoinstance.search_declaration (ConstRef kn) in
+  let () = Typeclasses.declare_instance None false gr in
+  let () = if is_coe then Class.try_add_new_coercion gr local in
+  Lib.is_modtype_strict ()
 
 let declare_assumptions_hook = ref ignore
 let set_declare_assumptions_hook = (:=) declare_assumptions_hook
@@ -399,7 +404,7 @@ let do_mutual_inductive indl finite =
   (* Declare the possible notations of inductive types *)
   List.iter Metasyntax.add_notation_interpretation ntns;
   (* Declare the coercions *)
-  List.iter (fun qid -> Class.try_add_new_coercion (locate qid) Global) coes
+  List.iter (fun qid -> Class.try_add_new_coercion (locate qid) false) coes
 
 (* 3c| Fixpoints and co-fixpoints *)
 
@@ -510,6 +515,7 @@ let declare_fix kind f def t imps =
     const_entry_opaque = false;
     const_entry_inline_code = false
   } in
+  (** FIXME: include locality *)
   let kn = declare_constant f (DefinitionEntry ce,IsDefinition kind) in
   let gr = ConstRef kn in
   Autoinstance.search_declaration (ConstRef kn);
@@ -704,6 +710,7 @@ let build_wellfounded (recname,n,bl,arityc,body) r measure notation =
         const_entry_opaque = false;
         const_entry_inline_code = false}
 	in 
+	(** FIXME: include locality *)
 	let c = Declare.declare_constant recname (DefinitionEntry ce, IsDefinition Definition) in
 	let gr = ConstRef c in
 	  if Impargs.is_implicit_args () || not (List.is_empty impls) then
diff --git a/toplevel/ind_tables.ml b/toplevel/ind_tables.ml
index e03c3e9b5..7cf60b7ff 100644
--- a/toplevel/ind_tables.ml
+++ b/toplevel/ind_tables.ml
@@ -123,18 +123,18 @@ let compute_name internal id =
 let define internal id c =
   let fd = declare_constant ~internal in
   let id = compute_name internal id in
-  let kn = fd id
-    (DefinitionEntry
-      { const_entry_body = c;
-        const_entry_secctx = None;
-        const_entry_type = None;
-        const_entry_opaque = false;
-	const_entry_inline_code = false
-      },
-      Decl_kinds.IsDefinition Scheme) in
-  (match internal with
+  let entry = {
+    const_entry_body = c;
+    const_entry_secctx = None;
+    const_entry_type = None;
+    const_entry_opaque = false;
+    const_entry_inline_code = false
+  } in
+  let kn = fd id (DefinitionEntry entry, Decl_kinds.IsDefinition Scheme) in
+  let () = match internal with
   | KernelSilent -> ()
-  | _-> definition_message id);
+  | _-> definition_message id
+  in
   kn
 
 let define_individual_scheme_base kind suff f internal idopt (mind,i as ind) =
diff --git a/toplevel/lemmas.ml b/toplevel/lemmas.ml
index bf8cbcc25..e1f17b571 100644
--- a/toplevel/lemmas.ml
+++ b/toplevel/lemmas.ml
@@ -166,14 +166,18 @@ let save id const do_guard (locality,kind) hook =
        const_entry_opaque = opacity } = const in
   let k = Kindops.logical_kind_of_goal_kind kind in
   let l,r = match locality with
-    | Local when Lib.sections_are_opened () ->
+    | Discharge when Lib.sections_are_opened () ->
 	let c = SectionLocalDef (pft, tpo, opacity) in
 	let _ = declare_variable id (Lib.cwd(), c, k) in
 	(Local, VarRef id)
-    | Local | Global ->
-        let kn = declare_constant id (DefinitionEntry const, k) in
+    | Local | Global | Discharge ->
+        let local = match locality with
+        | Local | Discharge -> true
+        | Global -> false
+        in
+        let kn = declare_constant id ~local (DefinitionEntry const, k) in
 	Autoinstance.search_declaration (ConstRef kn);
-	(Global, ConstRef kn) in
+	(locality, ConstRef kn) in
   Pfedit.delete_current_proof ();
   definition_message id;
   hook l r
@@ -191,41 +195,51 @@ let compute_proof_name locality = function
   | None ->
       next_global_ident_away default_thm_id (Pfedit.get_all_proof_names ()) 
 
-let save_remaining_recthms (local,kind) body opaq i (id,(t_i,(_,imps))) =
+let save_remaining_recthms (locality,kind) body opaq i (id,(t_i,(_,imps))) =
   match body with
   | None ->
-      (match local with
-      | Local ->
-          let impl=false in (* copy values from Vernacentries *)
+      (match locality with
+      | Discharge ->
+          let impl = false in (* copy values from Vernacentries *)
           let k = IsAssumption Conjectural in
           let c = SectionLocalAssum (t_i,impl) in
 	  let _ = declare_variable id (Lib.cwd(),c,k) in
-          (Local,VarRef id,imps)
-      | Global ->
+          (Discharge, VarRef id,imps)
+      | Local | Global ->
           let k = IsAssumption Conjectural in
-          let kn = declare_constant id (ParameterEntry (None,t_i,None), k) in
-          (Global,ConstRef kn,imps))
+          let local = match locality with
+          | Local -> true
+          | Global -> false
+          | Discharge -> assert false
+          in
+          let decl = (ParameterEntry (None,t_i,None), k) in
+          let kn = declare_constant id ~local decl in
+          (locality,ConstRef kn,imps))
   | Some body ->
       let k = Kindops.logical_kind_of_goal_kind kind in
       let body_i = match kind_of_term body with
         | Fix ((nv,0),decls) -> mkFix ((nv,i),decls)
         | CoFix (0,decls) -> mkCoFix (i,decls)
         | _ -> anomaly (Pp.str "Not a proof by induction") in
-      match local with
-      | Local ->
+      match locality with
+      | Discharge ->
 	  let c = SectionLocalDef (body_i, Some t_i, opaq) in
 	  let _ = declare_variable id (Lib.cwd(), c, k) in
-          (Local,VarRef id,imps)
-      | Global ->
-          let const =
-            { const_entry_body = body_i;
-              const_entry_secctx = None;
-              const_entry_type = Some t_i;
-              const_entry_opaque = opaq;
-	      const_entry_inline_code = false
-	    } in
-          let kn = declare_constant id (DefinitionEntry const, k) in
-          (Global,ConstRef kn,imps)
+          (Discharge,VarRef id,imps)
+      | Local | Global ->
+        let local = match locality with
+        | Local -> true
+        | Global -> false
+        | Discharge -> assert false
+        in
+        let const = { const_entry_body = body_i;
+            const_entry_secctx = None;
+            const_entry_type = Some t_i;
+            const_entry_opaque = opaq;
+            const_entry_inline_code = false
+        } in
+        let kn = declare_constant id ~local (DefinitionEntry const, k) in
+        (locality,ConstRef kn,imps)
 
 let save_hook = ref ignore
 let set_save_hook f = save_hook := f
@@ -345,8 +359,7 @@ let start_proof_com kind thms hook =
 let admit () =
   let (id,k,typ,hook) = Pfedit.current_proof_statement () in
   let e = Pfedit.get_used_variables(), typ, None in
-  let kn =
-    declare_constant id (ParameterEntry e,IsAssumption Conjectural) in
+  let kn = declare_constant id (ParameterEntry e,IsAssumption Conjectural) in
   Pfedit.delete_current_proof ();
   assumption_message id;
   hook Global (ConstRef kn)
diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml
index b4384e77b..74b387dfe 100644
--- a/toplevel/obligations.ml
+++ b/toplevel/obligations.ml
@@ -590,7 +590,8 @@ let declare_obligation prg obl body =
 	  const_entry_opaque = opaque;
 	  const_entry_inline_code = false} 
       in
-      let constant = Declare.declare_constant obl.obl_name
+    (** ppedrot: seems legit to have obligations as local *)
+      let constant = Declare.declare_constant obl.obl_name ~local:true
 	(DefinitionEntry ce,IsProof Property)
       in
 	if not opaque then
@@ -945,7 +946,8 @@ let admit_prog prg =
         match x.obl_body with
         | None ->
             let x = subst_deps_obl obls x in
-            let kn = Declare.declare_constant x.obl_name 
+            (** ppedrot: seems legit to have admitted obligations as local *)
+            let kn = Declare.declare_constant x.obl_name ~local:true
               (ParameterEntry (None, x.obl_type,None), IsAssumption Conjectural)
             in
               assumption_message x.obl_name;
diff --git a/toplevel/record.ml b/toplevel/record.ml
index 93868dbe3..b6181590e 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -214,7 +214,7 @@ let declare_projections indsp ?(kind=StructureComponent) ?name coers fieldimpls
 	      Impargs.maybe_declare_manual_implicits false refi impls;
 	      if coe then begin
 	        let cl = Class.class_of_global (IndRef indsp) in
-	        Class.try_add_new_coercion_with_source refi Global ~source:cl
+	        Class.try_add_new_coercion_with_source refi ~local:false ~source:cl
 	      end;
 	      let proj_args = (*Rel 1 refers to "x"*) paramargs@[mkRel 1] in
 	      let constr_fip = applist (constr_fi,proj_args) in
@@ -273,7 +273,7 @@ let declare_structure finite infer id idbuild paramimpls params arity fieldimpls
   let cstr = (rsp,1) in
   let kinds,sp_projs = declare_projections rsp ~kind ?name coers fieldimpls fields in
   let build = ConstructRef cstr in
-  if is_coe then Class.try_add_new_coercion build Global;
+  let () = if is_coe then Class.try_add_new_coercion build ~local:false in
   Recordops.declare_structure(rsp,cstr,List.rev kinds,List.rev sp_projs);
   if infer then
     Evd.fold (fun ev evi () -> Recordops.declare_method (ConstructRef cstr) ev sign) sign ();
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index e735dde0d..4c5e07a54 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -459,8 +459,10 @@ let vernac_definition_hook = function
 
 let vernac_definition (local,k) (loc,id as lid) def =
   let hook = vernac_definition_hook k in
-  if local == Local then Dumpglob.dump_definition lid true "var"
-  else Dumpglob.dump_definition lid false "def";
+  let () = match local with
+  | Discharge -> Dumpglob.dump_definition lid true "var"
+  | Local | Global -> Dumpglob.dump_definition lid false "def"
+  in
   (match def with
     | ProveBody (bl,t) ->   (* local binders, typ *)
  	  start_proof_and_print (local,DefinitionBody Definition)
@@ -768,13 +770,13 @@ let vernac_coercion stre ref qids qidt =
   let target = cl_of_qualid qidt in
   let source = cl_of_qualid qids in
   let ref' = smart_global ref in
-  Class.try_add_new_coercion_with_target ref' stre ~source ~target;
+  Class.try_add_new_coercion_with_target ref' ~local:stre ~source ~target;
   if_verbose msg_info (pr_global ref' ++ str " is now a coercion")
 
 let vernac_identity_coercion stre id qids qidt =
   let target = cl_of_qualid qidt in
   let source = cl_of_qualid qids in
-  Class.try_add_new_identity_coercion id stre ~source ~target
+  Class.try_add_new_identity_coercion id ~local:stre ~source ~target
 
 (* Type classes *)