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

1 files changed, 2 insertions, 2 deletions

diff --git a/contrib/correctness/ptactic.ml b/contrib/correctness/ptactic.ml
index aac393690..c24baea80 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 ());