Intégration des modifs de la branche mowgli :

- Simplification de strength qui est maintenant un simple drapeau Local/Global.
- Export des catégories de déclarations (Lemma/Theorem/Definition/.../
  Axiom/Parameter/..) vers les .vo (nouveau fichier library/decl_kinds.ml).
- Export des variables de section initialement associées à une déclaration
  (nouveau fichier library/dischargedhypsmap.ml).


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

4 files changed, 14 insertions, 11 deletions

diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index 36e0fa23f0..adc2054fe2 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -35,6 +35,7 @@ open Tactics
 open Inv
 open Vernacexpr
 open Safe_typing
+open Decl_kinds
 
 let not_work_message = "tactic fails to build the inversion lemma, may be because the predicate has arguments that depend on other arguments"
 
@@ -248,7 +249,7 @@ let add_inversion_lemma name env sigma t sort dep inv_op =
     (DefinitionEntry { const_entry_body = invProof;
                      const_entry_type = None;
                      const_entry_opaque = false }, 
-     Libnames.NeverDischarge)
+     IsProof Lemma)
   in ()
 
 (* open Pfedit *)
diff --git a/tactics/setoid_replace.ml b/tactics/setoid_replace.ml
index 8c2077f46c..3a4ae8e13b 100644
--- a/tactics/setoid_replace.ml
+++ b/tactics/setoid_replace.ml
@@ -30,6 +30,7 @@ open Tacticals
 open Vernacexpr
 open Safe_typing
 open Nametab
+open Decl_kinds
 
 type setoid =
     { set_a : constr;
@@ -297,12 +298,12 @@ let add_setoid a aeq th =
 		      ((DefinitionEntry {const_entry_body = eq_morph; 
 		                       const_entry_type = Some eq_morph_typ;
                                        const_entry_opaque = true}),
-		       Libnames.NeverDischarge) in
+		       IsProof Lemma) in
 	    let _ = Declare.declare_constant eq_ext_name2
 		      ((DefinitionEntry {const_entry_body = eq_morph2; 
 				       const_entry_type = Some eq_morph2_typ;
                                        const_entry_opaque = true}),
-		       Libnames.NeverDischarge) in
+		       IsProof Lemma) in
 	    let eqmorph = (current_constant eq_ext_name) in
 	    let eqmorph2 = (current_constant eq_ext_name2) in
 	      (Lib.add_anonymous_leaf
@@ -415,8 +416,7 @@ let new_morphism m id hook =
 	let lem = (gen_compat_lemma env m body args_t poss) in
 	let lemast = (ast_of_constr true env lem) in
 	new_edited id m poss;
-	start_proof_com (Some id) (false,Libnames.NeverDischarge)
-          ([],lemast) hook;
+	start_proof_com (Some id) (IsGlobal DefinitionBody) ([],lemast) hook;
 	(Options.if_verbose Vernacentries.show_open_subgoals ()))
 
 let rec sub_bool l1 n = function
@@ -511,7 +511,7 @@ let add_morphism lem_name (m,profil) =
 		    ((DefinitionEntry {const_entry_body = lem_2; 
 				     const_entry_type = None;
                                      const_entry_opaque = true}),
-		     Libnames.NeverDischarge) in
+		     IsProof Lemma) in
 	  let lem2 = (current_constant lem2_name) in
 	    (Lib.add_anonymous_leaf
 	       (morphism_to_obj (m, 
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 568ffd021d..efa497b951 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -40,6 +40,7 @@ open Safe_typing
 open Typing
 open Hiddentac
 open Genarg
+open Decl_kinds
 
 let err_msg_tactic_not_found macro_loc macro =
   user_err_loc
@@ -1277,7 +1278,7 @@ and letin_interp ist = function
            (match ist.goalopt with
            | None -> Global.named_context ()
            | Some g -> pf_hyps g) in
-         start_proof id (true,NeverDischarge) ndc typ (fun _ _ -> ());
+         start_proof id IsLocal ndc typ (fun _ _ -> ());
          by t;
          let (_,({const_entry_body = pft; const_entry_type = _},_,_)) =
            cook_proof () in
@@ -1324,7 +1325,7 @@ and letcut_interp ist = function
     | _ ->
       (try
          let t = tactic_of_value tac in
-         start_proof id (false,NeverDischarge) ndc typ (fun _ _ -> ());
+         start_proof id IsLocal ndc typ (fun _ _ -> ());
          by t;
          let (_,({const_entry_body = pft; const_entry_type = _},_,_)) =
            cook_proof () in
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index bca15185cd..5978e1070f 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -38,6 +38,7 @@ open Hipattern
 open Coqlib
 open Nametab
 open Tacexpr
+open Decl_kinds
 
 exception Bound
 
@@ -1622,8 +1623,8 @@ let abstract_subproof name tac gls =
   in
   if occur_existential concl then error "Abstract cannot handle existentials";
   let lemme =
-    start_proof na (false,NeverDischarge) current_sign concl (fun _ _ -> ());
-    let _,(const,(_,strength),_) =
+    start_proof na (IsGlobal (Proof Lemma)) current_sign concl (fun _ _ -> ());
+    let _,(const,kind,_) =
       try
 	by (tclCOMPLETE (tclTHEN (tclDO (List.length sign) intro) tac)); 
 	let r = cook_proof () in 
@@ -1632,7 +1633,7 @@ let abstract_subproof name tac gls =
 	(delete_current_proof(); raise e)
     in   (* Faudrait un peu fonctionnaliser cela *)
     let cd = Entries.DefinitionEntry const in
-    let sp = Declare.declare_constant na (cd,strength) in
+    let sp = Declare.declare_constant na (cd,IsProof Lemma) in
     let newenv = Global.env() in
     Declare.constr_of_reference (ConstRef (snd sp))
   in