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

2 files changed, 3 insertions, 3 deletions

diff --git a/contrib/correctness/psyntax.ml4 b/contrib/correctness/psyntax.ml4
index 59a32bafbb..591076bddb 100644
--- a/contrib/correctness/psyntax.ml4
+++ b/contrib/correctness/psyntax.ml4
@@ -548,7 +548,7 @@ let _ =
 	      if not (is_mutable v) then begin
 		let c = 
 		  Entries.ParameterEntry (trad_ml_type_v ren env v),
-		  Libnames.NeverDischarge in
+		  Decl_kinds.IsAssumption Decl_kinds.Definitional in
 		List.iter 
 		  (fun id -> ignore (Declare.declare_constant id c)) ids;
 		if_verbose (is_assumed false) ids
diff --git a/contrib/correctness/ptactic.ml b/contrib/correctness/ptactic.ml
index aac3936909..c24baea805 100644
--- a/contrib/correctness/ptactic.ml
+++ b/contrib/correctness/ptactic.ml
@@ -17,6 +17,7 @@ open Libnames
 open Term
 open Pretyping
 open Pfedit
+open Decl_kinds
 open Vernacentries
 
 open Pmisc
@@ -27,7 +28,6 @@ open Prename
 open Peffect
 open Pmonad
 
-
 (* [coqast_of_prog: program -> constr * constr]
  * Traduction d'un programme impératif en un but (second constr)
  * et un terme de preuve partiel pour ce but (premier constr)
@@ -239,7 +239,7 @@ let correctness s p opttac =
   let sigma = Evd.empty in
   let cty = Reduction.nf_betaiota cty in
   let id = id_of_string s in 
-  start_proof id (false, NeverDischarge) sign cty correctness_hook;
+  start_proof id (IsGlobal (Proof Lemma)) sign cty correctness_hook;
   Penv.new_edited id (v,p);
   if !debug then show_open_subgoals();
   deb_mess (str"Pred.red_cci: Reduction..." ++ fnl ());