Decl_kinds becomes a pure mli file, remaining ops in new file kindops.ml

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

2 files changed, 32 insertions, 40 deletions

diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index 60aa99b12..de7e17957 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -163,16 +163,16 @@ let save with_clean id const (locality,kind) hook =
        const_entry_opaque = opacity } = const in
   let l,r = match locality with
     | Local when Lib.sections_are_opened () ->
-        let k = logical_kind_of_goal_kind kind in
+        let k = Kindops.logical_kind_of_goal_kind kind in
 	let c = SectionLocalDef (pft, tpo, opacity) in
 	let _ = declare_variable id (Lib.cwd(), c, k) in
 	(Local, VarRef id)
     | Local ->
-        let k = logical_kind_of_goal_kind kind in
+        let k = Kindops.logical_kind_of_goal_kind kind in
         let kn = declare_constant id (DefinitionEntry const, k) in
 	(Global, ConstRef kn)
     | Global ->
-        let k = logical_kind_of_goal_kind kind in
+        let k = Kindops.logical_kind_of_goal_kind kind in
         let kn = declare_constant id (DefinitionEntry const, k) in
 	(Global, ConstRef kn) in
   if with_clean then  Pfedit.delete_current_proof ();
diff --git a/plugins/xml/xmlcommand.ml b/plugins/xml/xmlcommand.ml
index 13821488a..93ff00dff 100644
--- a/plugins/xml/xmlcommand.ml
+++ b/plugins/xml/xmlcommand.ml
@@ -64,12 +64,12 @@ let extract_nparams pack =
 
 *)
 
+open Decl_kinds
+
 (* could_have_namesakes sp = true iff o is an object that could be cooked and *)
 (* than that could exists in cooked form with the same name in a super        *)
 (* section of the actual section                                              *)
 let could_have_namesakes o sp =      (* namesake = omonimo in italian *)
- let module DK = Decl_kinds in
- let module D = Declare in
   let tag = Libobject.object_tag o in
    print_if_verbose ("Object tag: " ^ tag ^ "\n") ;
    match tag with
@@ -106,11 +106,6 @@ let filter_params pvars hyps =
    aux (Names.repr_dirpath modulepath) (List.rev pvars)
 ;;
 
-type variables_type =
-   Definition of string * Term.constr * Term.types
- | Assumption of string * Term.constr
-;;
-
 (* The computation is very inefficient, but we can't do anything *)
 (* better unless this function is reimplemented in the Declare   *)
 (* module.                                                       *)
@@ -401,9 +396,9 @@ let theory_output_string ?(do_not_quote = false) s =
 ;;
 
 let kind_of_global_goal = function
-  | Decl_kinds.Global, Decl_kinds.DefinitionBody _ -> "DEFINITION","InteractiveDefinition"
-  | Decl_kinds.Global, (Decl_kinds.Proof k) -> "THEOREM",Decl_kinds.string_of_theorem_kind k
-  | Decl_kinds.Local, _ -> assert false
+  | Global, DefinitionBody _ -> "DEFINITION","InteractiveDefinition"
+  | Global, (Proof k) -> "THEOREM",Kindops.string_of_theorem_kind k
+  | Local, _ -> assert false
 
 let kind_of_inductive isrecord kn =
  "DEFINITION",
@@ -417,68 +412,65 @@ let kind_of_inductive isrecord kn =
 ;;
 
 let kind_of_variable id =
-  let module DK = Decl_kinds in
   match Decls.variable_kind id with
-    | DK.IsAssumption DK.Definitional -> "VARIABLE","Assumption"
-    | DK.IsAssumption DK.Logical -> "VARIABLE","Hypothesis"
-    | DK.IsAssumption DK.Conjectural -> "VARIABLE","Conjecture"
-    | DK.IsDefinition DK.Definition -> "VARIABLE","LocalDefinition"
-    | DK.IsProof _ -> "VARIABLE","LocalFact"
+    | IsAssumption Definitional -> "VARIABLE","Assumption"
+    | IsAssumption Logical -> "VARIABLE","Hypothesis"
+    | IsAssumption Conjectural -> "VARIABLE","Conjecture"
+    | IsDefinition Definition -> "VARIABLE","LocalDefinition"
+    | IsProof _ -> "VARIABLE","LocalFact"
     | _ -> Errors.anomaly "Unsupported variable kind"
 ;;
 
 let kind_of_constant kn =
-  let module DK = Decl_kinds in
   match Decls.constant_kind kn with
-    | DK.IsAssumption DK.Definitional -> "AXIOM","Declaration"
-    | DK.IsAssumption DK.Logical -> "AXIOM","Axiom"
-    | DK.IsAssumption DK.Conjectural ->
+    | IsAssumption Definitional -> "AXIOM","Declaration"
+    | IsAssumption Logical -> "AXIOM","Axiom"
+    | IsAssumption Conjectural ->
         Pp.warning "Conjecture not supported in dtd (used Declaration instead)";
         "AXIOM","Declaration"
-    | DK.IsDefinition DK.Definition -> "DEFINITION","Definition"
-    | DK.IsDefinition DK.Example ->
+    | IsDefinition Definition -> "DEFINITION","Definition"
+    | IsDefinition Example ->
         Pp.warning "Example not supported in dtd (used Definition instead)";
         "DEFINITION","Definition"
-    | DK.IsDefinition DK.Coercion ->
+    | IsDefinition Coercion ->
         Pp.warning "Coercion not supported in dtd (used Definition instead)";
         "DEFINITION","Definition"
-    | DK.IsDefinition DK.SubClass ->
+    | IsDefinition SubClass ->
         Pp.warning "SubClass not supported in dtd (used Definition instead)";
         "DEFINITION","Definition"
-    | DK.IsDefinition DK.CanonicalStructure ->
+    | IsDefinition CanonicalStructure ->
         Pp.warning "CanonicalStructure not supported in dtd (used Definition instead)";
         "DEFINITION","Definition"
-    | DK.IsDefinition DK.Fixpoint ->
+    | IsDefinition Fixpoint ->
         Pp.warning "Fixpoint not supported in dtd (used Definition instead)";
         "DEFINITION","Definition"
-    | DK.IsDefinition DK.CoFixpoint ->
+    | IsDefinition CoFixpoint ->
         Pp.warning "CoFixpoint not supported in dtd (used Definition instead)";
         "DEFINITION","Definition"
-    | DK.IsDefinition DK.Scheme ->
+    | IsDefinition Scheme ->
         Pp.warning "Scheme not supported in dtd (used Definition instead)";
         "DEFINITION","Definition"
-    | DK.IsDefinition DK.StructureComponent ->
+    | IsDefinition StructureComponent ->
         Pp.warning "StructureComponent not supported in dtd (used Definition instead)";
         "DEFINITION","Definition"
-    | DK.IsDefinition DK.IdentityCoercion ->
+    | IsDefinition IdentityCoercion ->
         Pp.warning "IdentityCoercion not supported in dtd (used Definition instead)";
         "DEFINITION","Definition"
-    | DK.IsDefinition DK.Instance ->
+    | IsDefinition Instance ->
         Pp.warning "Instance not supported in dtd (used Definition instead)";
         "DEFINITION","Definition"
-    | DK.IsDefinition DK.Method ->
+    | IsDefinition Method ->
         Pp.warning "Method not supported in dtd (used Definition instead)";
         "DEFINITION","Definition"
-    | DK.IsProof (DK.Theorem|DK.Lemma|DK.Corollary|DK.Fact|DK.Remark as thm) ->
-        "THEOREM",DK.string_of_theorem_kind thm
-    | DK.IsProof _ ->
+    | IsProof (Theorem|Lemma|Corollary|Fact|Remark as thm) ->
+        "THEOREM",Kindops.string_of_theorem_kind thm
+    | IsProof _ ->
         Pp.warning "Unsupported theorem kind (used Theorem instead)";
-        "THEOREM",DK.string_of_theorem_kind DK.Theorem
+        "THEOREM",Kindops.string_of_theorem_kind Theorem
 ;;
 
 let kind_of_global r =
   let module Ln = Libnames in
-  let module DK = Decl_kinds in
   match r with
   | Ln.IndRef kn | Ln.ConstructRef (kn,_) ->
       let isrecord =