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

5 files changed, 22 insertions, 31 deletions

diff --git a/contrib/correctness/psyntax.ml4 b/contrib/correctness/psyntax.ml4
index 59a32bafb..591076bdd 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 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 ());
diff --git a/contrib/interface/centaur.ml4 b/contrib/interface/centaur.ml4
index b1602655f..b917f24d4 100644
--- a/contrib/interface/centaur.ml4
+++ b/contrib/interface/centaur.ml4
@@ -417,7 +417,7 @@ let inspect n =
              	oname, Lib.Leaf lobj ->
 		  (match oname, object_tag lobj with
                        (sp,_), "VARIABLE" ->
-			 let ((_, _, v), _) = get_variable (basename sp) in
+			 let (_, _, v) = get_variable (basename sp) in
 			   add_search2 (Nametab.locate (qualid_of_sp sp)) v
 		     | (sp,kn), ("CONSTANT"|"PARAMETER") ->
 			 let {const_type=typ} = Global.lookup_constant kn in
diff --git a/contrib/interface/name_to_ast.ml b/contrib/interface/name_to_ast.ml
index ef232d0dc..ec600d21d 100644
--- a/contrib/interface/name_to_ast.ml
+++ b/contrib/interface/name_to_ast.ml
@@ -19,6 +19,7 @@ open Pp;;
 open Declare;;
 open Nametab
 open Vernacexpr;;
+open Decl_kinds;;
 
 (* This function converts the parameter binders of an inductive definition,
    in particular you have to be careful to handle each element in the
@@ -150,7 +151,7 @@ let make_variable_ast name typ implicits =
 *)
 let make_variable_ast name typ implicits =
   (VernacAssumption
-    (AssumptionVariable, [false,(name, constr_to_ast (body_of_type typ))]))
+    ((Local,Definitional), [false,(name, constr_to_ast (body_of_type typ))]))
   ::(implicits_to_ast_list implicits);;
     
 (*
@@ -165,7 +166,7 @@ let make_definition_ast name c typ implicits =
   (implicits_to_ast_list implicits);;
 *)
 let make_definition_ast name c typ implicits =
-  VernacDefinition (Definition, name, DefineBody ([], None,
+  VernacDefinition (Global, name, DefineBody ([], None,
     (constr_to_ast c), Some (constr_to_ast (body_of_type typ))),
     (fun _ _ -> ()))
   ::(implicits_to_ast_list implicits);;
@@ -183,7 +184,7 @@ let constant_to_ast_list kn =
 	make_definition_ast (id_of_label (label kn)) (Declarations.force c1) typ l)
 
 let variable_to_ast_list sp =
-  let ((id, c, v), _) = get_variable sp in
+  let (id, c, v) = get_variable sp in
   let l = implicits_of_var sp in
     (match c with
 	 None -> 
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index 7142f1e6d..92a35b892 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -12,6 +12,7 @@ open Genarg;;
 open Rawterm;;
 open Tacexpr;;
 open Vernacexpr;;
+open Decl_kinds;;
 
 let in_coq_ref = ref false;;
 
@@ -1467,27 +1468,18 @@ let xlate_thm x = CT_thm (match x with
   | Theorem -> "Theorem"
   | Remark -> "Remark"
   | Lemma -> "Lemma"
-  | Fact -> "Fact"
-  | Decl -> "Decl")
+  | Fact -> "Fact")
 
 
 let xlate_defn x = CT_defn (match x with
- | LocalDefinition -> "Local"
- | Definition -> "Definition")
-
-
-let xlate_defn_or_thm =
-  function
- (* Unable to decide if a fact in one section or at toplevel, a remark
-    at toplevel or a theorem or a Definition *)
- | StartTheoremProof k -> CT_coerce_THM_to_DEFN_OR_THM (xlate_thm k)
- | StartDefinitionBody k -> CT_coerce_DEFN_to_DEFN_OR_THM (xlate_defn k);;
+ | Local -> "Local"
+ | Global -> "Definition")
 
 let xlate_var x = CT_var (match x with
- | AssumptionParameter -> "Parameter"
- | AssumptionAxiom -> "Axiom"
- | AssumptionVariable -> "Variable"
- | AssumptionHypothesis -> "Hypothesis");;
+ | (Global,Definitional) -> "Parameter"
+ | (Global,Logical) -> "Axiom"
+ | (Local,Definitional) -> "Variable"
+ | (Local,Logical) -> "Hypothesis");;
 
 
 let xlate_dep =
@@ -1915,8 +1907,7 @@ let xlate_vernac =
 
    | VernacNotation _ -> xlate_error "TODO: Notation"
 
-   | VernacInfix (str_assoc, n, str, id, sc) ->
-      (* TODO: handle scopes *)
+   | VernacInfix (str_assoc, n, str, id, None) ->
       CT_infix (
        (match str_assoc with
         | Some Gramext.LeftA -> CT_lefta
@@ -1924,15 +1915,15 @@ let xlate_vernac =
         | Some Gramext.NonA -> CT_nona
         | None -> CT_coerce_NONE_to_ASSOC CT_none),
        CT_int n, CT_string str, loc_qualid_to_ct_ID id)
+   | VernacInfix _ -> xlate_error "TODO: handle scopes"
    | VernacGrammar _ -> xlate_error "GRAMMAR not implemented"
    | VernacCoercion (s, id1, id2, id3) ->
       let id_opt = CT_coerce_NONE_to_IDENTITY_OPT CT_none in
       let local_opt =
        match s with
        (* Cannot decide whether it is a global or a Local but at toplevel *)
-       | Libnames.NeverDischarge -> CT_coerce_NONE_to_LOCAL_OPT CT_none
-       | Libnames.DischargeAt _ -> CT_local
-       | Libnames.NotDeclare -> assert false in
+       | Global -> CT_coerce_NONE_to_LOCAL_OPT CT_none
+       | Local -> CT_local in
       CT_coercion (local_opt, id_opt, loc_qualid_to_ct_ID id1,
         xlate_class id2, xlate_class id3)
 
@@ -1941,9 +1932,8 @@ let xlate_vernac =
       let local_opt =
        match s with
        (* Cannot decide whether it is a global or a Local but at toplevel *)
-       | Libnames.NeverDischarge -> CT_coerce_NONE_to_LOCAL_OPT CT_none
-       | Libnames.DischargeAt _ -> CT_local 
-       | Libnames.NotDeclare -> assert false in
+       | Global -> CT_coerce_NONE_to_LOCAL_OPT CT_none
+       | Local -> CT_local in
       CT_coercion (local_opt, id_opt, xlate_ident id1,
         xlate_class id2, xlate_class id3)
   | VernacResetName id -> CT_reset (xlate_ident id)