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

2 files changed, 19 insertions, 18 deletions

diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index 942cdc77e0..c8a3ffd55d 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -225,17 +225,15 @@ let inversion_scheme env sigma t sort dep_option inv_op =
 
 let add_inversion_lemma name env sigma t sort dep inv_op =
   let invProof = inversion_scheme env sigma t sort dep inv_op in
-  let _ =
-    declare_constant name
-    (DefinitionEntry
-       { const_entry_body = invProof;
-         const_entry_secctx = None;
-         const_entry_type = None;
-         const_entry_opaque = false;
-	 const_entry_inline_code = false	   
-       },
-     IsProof Lemma)
-  in ()
+  let entry = {
+    const_entry_body = invProof;
+    const_entry_secctx = None;
+    const_entry_type = None;
+    const_entry_opaque = false;
+    const_entry_inline_code = false;
+  } in
+  let _ = declare_constant name (DefinitionEntry entry, IsProof Lemma) in
+  ()
 
 (* inv_op = Inv (derives de complete inv. lemma)
  * inv_op = InvNoThining (derives de semi inversion lemma) *)
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 6ba5e0e04f..a3733b3e77 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -3528,7 +3528,10 @@ let abstract_subproof id tac gl =
   let const = Pfedit.build_constant_by_tactic id secsign concl
     (tclCOMPLETE (tclTHEN (tclDO (List.length sign) intro) tac)) in
   let cd = Entries.DefinitionEntry const in
-  let lem = mkConst (Declare.declare_constant ~internal:Declare.KernelSilent id (cd,IsProof Lemma)) in
+  let decl = (cd, IsProof Lemma) in
+  (** ppedrot: seems legit to have abstracted subproofs as local*)
+  let cst = Declare.declare_constant ~internal:Declare.KernelSilent ~local:true id decl in
+  let lem = mkConst cst in
   exact_no_check
     (applist (lem,List.rev (Array.to_list (instance_from_named_context sign))))
     gl
@@ -3556,12 +3559,12 @@ let admit_as_an_axiom gl =
   let na = next_global_ident_away name (pf_ids_of_hyps gl) in
   let concl = it_mkNamedProd_or_LetIn (pf_concl gl) sign in
   if occur_existential concl then error"\"admit\" cannot handle existentials.";
-  let axiom =
-    let cd = 
-      Entries.ParameterEntry (Pfedit.get_used_variables(),concl,None) in
-    let con = Declare.declare_constant ~internal:Declare.KernelSilent na (cd,IsAssumption Logical) in
-    constr_of_global (ConstRef con)
-  in
+  let entry = (Pfedit.get_used_variables (), concl, None) in
+  let cd = Entries.ParameterEntry entry in
+  let decl = (cd, IsAssumption Logical) in
+  (** ppedrot: seems legit to have admitted subproofs as local*)
+  let con = Declare.declare_constant ~internal:Declare.KernelSilent ~local:true na decl in
+  let axiom = constr_of_global (ConstRef con) in
   exact_no_check
     (applist (axiom,
               List.rev (Array.to_list (instance_from_named_context sign))))