aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins
diff options
context:
space:
mode:
authorGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2012-05-29 11:08:17 +0000
committerGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2012-05-29 11:08:17 +0000
commit69929de6eccf6d60886ea0795376e9288863fc1f (patch)
tree0c63bd8295976a7f7dd2a996bfb748ef30196e66 /plugins
parent442feb2c07f8f5824e814bba504f02c2742637e2 (diff)
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
Diffstat (limited to 'plugins')
-rw-r--r--plugins/funind/indfun_common.ml6
-rw-r--r--plugins/xml/xmlcommand.ml66
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 =