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, 25 insertions, 41 deletions

diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index c3afc0956..a7eae13ee 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -19,6 +19,7 @@ open Util
 open Constr
 open Vernac_
 open Prim
+open Decl_kinds
 
 (* Dans join_binders, s'il y a un "?", on perd l'info qu'il est partag�� *)
 let join_binders (idl,c) = List.map (fun id -> (id,c)) idl
@@ -97,26 +98,24 @@ GEXTEND Gram
     [ [ "Theorem" -> Theorem
       | IDENT "Lemma" -> Lemma
       | IDENT "Fact" -> Fact
-      | IDENT "Remark" -> Remark
-      | IDENT "Decl" -> Decl ] ]
+      | IDENT "Remark" -> Remark ] ]
   ;
   def_token:
-    [ [ "Definition" -> (fun _ _ -> ()), Definition
-      | IDENT "Local" -> (fun _ _ -> ()), LocalDefinition
-      | IDENT "SubClass"  -> Class.add_subclass_hook, Definition
-      | IDENT "Local"; IDENT "SubClass"  ->
-	  Class.add_subclass_hook, LocalDefinition ] ]  
+    [ [ "Definition" -> (fun _ _ -> ()), Global
+      | IDENT "Local" -> (fun _ _ -> ()), Local
+      | IDENT "SubClass"  -> Class.add_subclass_hook, Global
+      | IDENT "Local"; IDENT "SubClass"  -> Class.add_subclass_hook, Local ] ] 
   ;
   assumption_token:
-    [ [ "Hypothesis" -> AssumptionHypothesis
-      | "Variable" -> AssumptionVariable
-      | "Axiom" -> AssumptionAxiom
-      | "Parameter" -> AssumptionParameter ] ]
+    [ [ "Hypothesis" -> (Local, Logical)
+      | "Variable" -> (Local, Definitional)
+      | "Axiom" -> (Global, Logical)
+      | "Parameter" -> (Global, Definitional) ] ]
   ;
   assumptions_token:
-    [ [ IDENT "Hypotheses" -> AssumptionHypothesis
-      | IDENT "Variables" -> AssumptionVariable
-      | IDENT "Parameters" -> AssumptionParameter ] ]
+    [ [ IDENT "Hypotheses" -> (Local, Logical)
+      | IDENT "Variables" -> (Local, Definitional)
+      | IDENT "Parameters" -> (Global, Definitional) ] ]
   ;
   of_type_with_opt_coercion:
     [ [ ":>" -> true
@@ -357,35 +356,29 @@ ident_comma_list_tail:
 	  VernacCanonical qid
       | IDENT "Canonical"; IDENT "Structure"; qid = qualid; d = def_body ->
           let s = Ast.coerce_qualid_to_id qid in
-	  VernacDefinition (Definition,s,d,Recordobj.add_object_hook)
-(*
-	  VernacDefinition (Definition,s,None,c,t,Recordobj.add_object_hook)
-*)
+	  VernacDefinition (Global,s,d,Recordobj.add_object_hook)
       (* Rem: LOBJECT, OBJCOERCION, LOBJCOERCION have been removed
          (they were unused and undocumented) *)
 
 (* Coercions *)
       | IDENT "Coercion"; qid = qualid; d = def_body ->
           let s = Ast.coerce_qualid_to_id qid in
-(*
-	  VernacDefinition (Definition,s,None,c,t,Class.add_coercion_hook)
-*)
-	  VernacDefinition (Definition,s,d,Class.add_coercion_hook)
+	  VernacDefinition (Global,s,d,Class.add_coercion_hook)
       | IDENT "Coercion"; IDENT "Local"; qid = qualid; d = def_body ->
            let s = Ast.coerce_qualid_to_id qid in
-	  VernacDefinition (LocalDefinition,s,d,Class.add_coercion_hook)
+	  VernacDefinition (Local,s,d,Class.add_coercion_hook)
       | IDENT "Identity"; IDENT "Coercion"; IDENT "Local"; f = Prim.ident;
          ":"; s = class_rawexpr; ">->"; t = class_rawexpr -> 
-	   VernacIdentityCoercion (Declare.make_strength_0 (), f, s, t)
+	   VernacIdentityCoercion (Local, f, s, t)
       | IDENT "Identity"; IDENT "Coercion"; f = Prim.ident; ":";
          s = class_rawexpr; ">->"; t = class_rawexpr -> 
-	   VernacIdentityCoercion (Libnames.NeverDischarge, f, s, t)
+	   VernacIdentityCoercion (Global, f, s, t)
       | IDENT "Coercion"; IDENT "Local"; qid = qualid; ":";
 	 s = class_rawexpr; ">->"; t = class_rawexpr -> 
-	  VernacCoercion (Declare.make_strength_0 (), qid, s, t)
+	  VernacCoercion (Local, qid, s, t)
       | IDENT "Coercion"; qid = qualid; ":"; s = class_rawexpr; ">->";
          t = class_rawexpr ->
-	  VernacCoercion (Libnames.NeverDischarge, qid, s, t)
+	  VernacCoercion (Global, qid, s, t)
       | IDENT "Class"; IDENT "Local"; c = qualid ->
 	  Pp.warning "Class is obsolete"; VernacNop
       | IDENT "Class"; c = qualid ->
diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4
index d72a06f2a..67322863a 100644
--- a/parsing/pcoq.ml4
+++ b/parsing/pcoq.ml4
@@ -13,7 +13,6 @@ open Util
 open Ast
 open Genarg
 open Tacexpr
-open Vernacexpr
 
 (* The lexer of Coq *)
 
@@ -75,6 +74,7 @@ type typed_entry = entry_type Gramobj.entry
 
 module type Gramtypes =
 sig
+  open Decl_kinds
   val inAstListType : Coqast.t list G.Entry.e -> typed_entry
   val inTacticAtomAstType : raw_atomic_tactic_expr G.Entry.e -> typed_entry
   val inThmTokenAstType : theorem_kind G.Entry.e -> typed_entry
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index eb49b403c..b4a5bc9a7 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -175,8 +175,7 @@ module Tactic :
 
 module Vernac_ :
   sig
-    open Util
-    open Libnames
+    open Decl_kinds
     val thm_token : theorem_kind Gram.Entry.e
     val class_rawexpr : class_rawexpr Gram.Entry.e
     val gallina : vernac_expr Gram.Entry.e
@@ -185,7 +184,4 @@ module Vernac_ :
     val syntax : vernac_expr Gram.Entry.e
     val vernac : vernac_expr Gram.Entry.e
     val vernac_eoi : vernac_expr Gram.Entry.e
-(*
-    val reduce : Coqast.t list Gram.Entry.e
-*)
   end
diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml
index 55611ec28..0f1157f1d 100644
--- a/parsing/prettyp.ml
+++ b/parsing/prettyp.ml
@@ -263,7 +263,7 @@ let print_mutual sp =
              implicit_args_msg sp mipv))
 *)
 let print_section_variable sp =
-  let (d,_) = get_variable sp in
+  let d = get_variable sp in
   let l = implicits_of_var sp in
   (print_named_decl d ++ print_impl_args l)
 
@@ -489,7 +489,7 @@ let print_local_context () =
     | [] -> (mt ())
     | (oname,Lib.Leaf lobj)::rest ->
 	if "VARIABLE" = object_tag lobj then
-          let (d,_) = get_variable (basename (fst oname)) in 
+          let d = get_variable (basename (fst oname)) in 
 	  (print_var_rec rest ++
              print_named_decl d)
 	else 
@@ -547,11 +547,6 @@ let inspect depth =
 
 open Classops
 
-let string_of_strength = function
-  | NotDeclare -> "(temp)"
-  | NeverDischarge -> "(global)"
-  | DischargeAt (sp,_) -> "(disch@"^(string_of_dirpath sp)
-
 let print_coercion_value v = prterm (get_coercion_value v)
 
 let print_index_coercion c = 
diff --git a/parsing/search.ml b/parsing/search.ml
index 78e549e13..e1723a1d1 100644
--- a/parsing/search.ml
+++ b/parsing/search.ml
@@ -56,7 +56,7 @@ let crible (fn : global_reference -> env -> constr -> unit) ref =
     match object_tag lobj with
       | "VARIABLE" ->
 	  (try 
-	     let ((idc,_,typ),_) = get_variable (basename sp) in 
+	     let (idc,_,typ) = get_variable (basename sp) in 
              if (head_const typ) = const then fn (VarRef idc) env typ
 	   with Not_found -> (* we are in a section *) ())
       | "CONSTANT"