diff options
47 files changed, 266 insertions, 262 deletions
diff --git a/doc/plugin_tutorial/tuto1/src/simple_declare.ml b/doc/plugin_tutorial/tuto1/src/simple_declare.ml index 68ae5628db..9dd4700db5 100644 --- a/doc/plugin_tutorial/tuto1/src/simple_declare.ml +++ b/doc/plugin_tutorial/tuto1/src/simple_declare.ml @@ -9,4 +9,4 @@ let edeclare ?hook ~name ~poly ~scope ~kind ~opaque sigma udecl body tyopt imps let declare_definition ~poly name sigma body = let udecl = UState.default_univ_decl in edeclare ~name ~poly ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior) - ~kind:Decl_kinds.Definition ~opaque:false sigma udecl body None [] + ~kind:Decls.Definition ~opaque:false sigma udecl body None [] diff --git a/library/decls.ml b/interp/decls.ml index 5cb35323dd..933aa774b4 100644 --- a/library/decls.ml +++ b/interp/decls.ml @@ -12,18 +12,69 @@ associated declarations *) open Names -open Decl_kinds open Libnames -(** Datas associated to section variables and local definitions *) +type theorem_kind = + | Theorem + | Lemma + | Fact + | Remark + | Property + | Proposition + | Corollary -type variable_data = { - path:DirPath.t; - opaque:bool; - univs:Univ.ContextSet.t; - poly:bool; - kind:logical_kind; -} +type definition_object_kind = + | Definition + | Coercion + | SubClass + | CanonicalStructure + | Example + | Fixpoint + | CoFixpoint + | Scheme + | StructureComponent + | IdentityCoercion + | Instance + | Method + | Let + +type assumption_object_kind = Definitional | Logical | Conjectural | Context + +(* [assumption_kind] + + | Local | Global + ------------------------------------ + Definitional | Variable | Parameter + Logical | Hypothesis | Axiom + +*) +(** Kinds used in proofs *) + +type goal_object_kind = + | DefinitionBody of definition_object_kind + | Proof of theorem_kind + +(** Kinds used in library *) + +type logical_kind = + | IsPrimitive + | IsAssumption of assumption_object_kind + | IsDefinition of definition_object_kind + | IsProof of theorem_kind + +let logical_kind_of_goal_kind = function + | DefinitionBody d -> IsDefinition d + | Proof s -> IsProof s + +(** Data associated to section variables and local definitions *) + +type variable_data = + { path:DirPath.t + ; opaque:bool + ; univs:Univ.ContextSet.t + ; poly:bool + ; kind:logical_kind + } let vartab = Summary.ref (Id.Map.empty : variable_data Id.Map.t) ~name:"VARIABLE" diff --git a/library/decls.mli b/interp/decls.mli index f88958bb04..570f03bbce 100644 --- a/library/decls.mli +++ b/interp/decls.mli @@ -10,7 +10,57 @@ open Names open Libnames -open Decl_kinds + +type theorem_kind = + | Theorem + | Lemma + | Fact + | Remark + | Property + | Proposition + | Corollary + +type definition_object_kind = + | Definition + | Coercion + | SubClass + | CanonicalStructure + | Example + | Fixpoint + | CoFixpoint + | Scheme + | StructureComponent + | IdentityCoercion + | Instance + | Method + | Let + +type assumption_object_kind = Definitional | Logical | Conjectural | Context + +(* [assumption_kind] + + | Local | Global + ------------------------------------ + Definitional | Variable | Parameter + Logical | Hypothesis | Axiom + +*) +(** Kinds used in proofs *) + +type goal_object_kind = + | DefinitionBody of definition_object_kind + | Proof of theorem_kind + +(** Kinds used in library *) + +type logical_kind = + | IsPrimitive + | IsAssumption of assumption_object_kind + | IsDefinition of definition_object_kind + | IsProof of theorem_kind + +(** Operations *) +val logical_kind_of_goal_kind : goal_object_kind -> logical_kind (** This module manages non-kernel informations about declarations. It is either non-logical informations or logical informations that @@ -18,24 +68,33 @@ open Decl_kinds (** Registration and access to the table of variable *) -type variable_data = { - path:DirPath.t; - opaque:bool; - univs:Univ.ContextSet.t; - poly:bool; - kind:logical_kind; -} +type variable_data = + { path:DirPath.t + ; opaque:bool + ; univs:Univ.ContextSet.t + ; poly:bool + ; kind:logical_kind + } val add_variable_data : variable -> variable_data -> unit + +(* Not used *) val variable_path : variable -> DirPath.t + +(* Only used in dumpglob *) val variable_secpath : variable -> qualid val variable_kind : variable -> logical_kind + +(* User in Lemma, Very dubious *) val variable_opacity : variable -> bool + +(* Used in declare, very dubious *) val variable_context : variable -> Univ.ContextSet.t val variable_polymorphic : variable -> bool val variable_exists : variable -> bool (** Registration and access to the table of constants *) +(* Only used in dumpglob *) val add_constant_kind : Constant.t -> logical_kind -> unit val constant_kind : Constant.t -> logical_kind diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml index e1269025a4..53baf137cf 100644 --- a/interp/dumpglob.ml +++ b/interp/dumpglob.ml @@ -69,7 +69,7 @@ let previous_state = ref MultFiles let pause () = previous_state := !glob_output; glob_output := NoGlob let continue () = glob_output := !previous_state -open Decl_kinds +open Decls open Declarations let type_of_logical_kind = function diff --git a/interp/interp.mllib b/interp/interp.mllib index 33573edcce..cb6c527c83 100644 --- a/interp/interp.mllib +++ b/interp/interp.mllib @@ -10,6 +10,7 @@ Notation Syntax_def Smartlocate Constrexpr_ops +Decls Dumpglob Reserve Impargs diff --git a/library/decl_kinds.ml b/library/decl_kinds.ml index 6eb582baef..5c479255df 100644 --- a/library/decl_kinds.ml +++ b/library/decl_kinds.ml @@ -15,51 +15,3 @@ type binding_kind = Explicit | Implicit type private_flag = bool type cumulative_inductive_flag = bool - -type theorem_kind = - | Theorem - | Lemma - | Fact - | Remark - | Property - | Proposition - | Corollary - -type definition_object_kind = - | Definition - | Coercion - | SubClass - | CanonicalStructure - | Example - | Fixpoint - | CoFixpoint - | Scheme - | StructureComponent - | IdentityCoercion - | Instance - | Method - | Let - -type assumption_object_kind = Definitional | Logical | Conjectural | Context - -(* [assumption_kind] - - | Local | Global - ------------------------------------ - Definitional | Variable | Parameter - Logical | Hypothesis | Axiom - -*) -(** Kinds used in proofs *) - -type goal_object_kind = - | DefinitionBody of definition_object_kind - | Proof of theorem_kind - -(** Kinds used in library *) - -type logical_kind = - | IsPrimitive - | IsAssumption of assumption_object_kind - | IsDefinition of definition_object_kind - | IsProof of theorem_kind diff --git a/library/kindops.ml b/library/kindops.ml deleted file mode 100644 index 0bf55c62a9..0000000000 --- a/library/kindops.ml +++ /dev/null @@ -1,37 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) - -open Decl_kinds - -(** Operations about types defined in [Decl_kinds] *) - -let logical_kind_of_goal_kind = function - | DefinitionBody d -> IsDefinition d - | Proof s -> IsProof s - -let string_of_theorem_kind = function - | Theorem -> "Theorem" - | Lemma -> "Lemma" - | Fact -> "Fact" - | Remark -> "Remark" - | Property -> "Property" - | Proposition -> "Proposition" - | Corollary -> "Corollary" - -let string_of_definition_object_kind = function - | Definition -> "Definition" - | Example -> "Example" - | Coercion -> "Coercion" - | SubClass -> "SubClass" - | CanonicalStructure -> "Canonical Structure" - | Instance -> "Instance" - | Let -> "Let" - | (StructureComponent|Scheme|CoFixpoint|Fixpoint|IdentityCoercion|Method) -> - CErrors.anomaly (Pp.str "Internal definition kind.") diff --git a/library/kindops.mli b/library/kindops.mli deleted file mode 100644 index 3c9f2bb7c3..0000000000 --- a/library/kindops.mli +++ /dev/null @@ -1,17 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) - -open Decl_kinds - -(** Operations about types defined in [Decl_kinds] *) - -val logical_kind_of_goal_kind : goal_object_kind -> logical_kind -val string_of_theorem_kind : theorem_kind -> string -val string_of_definition_object_kind : definition_object_kind -> string diff --git a/library/library.mllib b/library/library.mllib index ef53471377..35af5fa43b 100644 --- a/library/library.mllib +++ b/library/library.mllib @@ -1,16 +1,15 @@ +Decl_kinds Libnames Globnames Libobject Summary Nametab Global -Decl_kinds Lib Declaremods Library States Kindops Goptions -Decls Keys Coqlib diff --git a/plugins/derive/derive.ml b/plugins/derive/derive.ml index e34150f2b3..780cf4af21 100644 --- a/plugins/derive/derive.ml +++ b/plugins/derive/derive.ml @@ -20,7 +20,7 @@ let start_deriving f suchthat name : Lemmas.t = let env = Global.env () in let sigma = Evd.from_env env in let poly = false in - let kind = Decl_kinds.(DefinitionBody Definition) in + let kind = Decls.(DefinitionBody Definition) in (* create a sort variable for the type of [f] *) (* spiwack: I don't know what the rigidity flag does, picked the one diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index f773b2c39e..6a5307d8f5 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -992,7 +992,7 @@ let generate_equation_lemma evd fnames f fun_num nb_params nb_args rec_args_num (* Pp.msgnl (str "lemma type (2) " ++ Printer.pr_lconstr_env (Global.env ()) evd lemma_type); *) let info = Lemmas.Info.make ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior) - ~kind:(Decl_kinds.Proof Decl_kinds.Theorem) () in + ~kind:(Decls.(Proof Theorem)) () in let lemma = Lemmas.start_lemma (*i The next call to mk_equation_id is valid since we are constructing the lemma diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index 3bab750534..87910eeae7 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -371,7 +371,7 @@ let generate_functional_principle (evd: Evd.evar_map ref) Declare.declare_constant name (Declare.DefinitionEntry ce, - Decl_kinds.IsDefinition (Decl_kinds.Scheme)) + Decls.(IsDefinition Scheme)) ); Declare.definition_message name; names := name :: !names @@ -387,7 +387,7 @@ let generate_functional_principle (evd: Evd.evar_map ref) Don't forget to close the goal if an error is raised !!!! *) let uctx = Evd.evar_universe_context sigma in - save new_princ_name entry ~hook uctx (DeclareDef.Global Declare.ImportDefaultBehavior) Decl_kinds.(Proof Theorem) + save new_princ_name entry ~hook uctx (DeclareDef.Global Declare.ImportDefaultBehavior) Decls.(Proof Theorem) with e when CErrors.noncritical e -> raise (Defining_principle e) @@ -638,7 +638,7 @@ let build_scheme fas = ignore (Declare.declare_constant princ_id - (Declare.DefinitionEntry def_entry,Decl_kinds.IsProof Decl_kinds.Theorem)); + (Declare.DefinitionEntry def_entry,Decls.(IsProof Theorem))); Declare.definition_message princ_id ) fas diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index d305a58ccc..9a9e0b9692 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -419,7 +419,7 @@ let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexp ~name:fname ~poly:false ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior) - ~kind:Decl_kinds.Definition pl + ~kind:Decls.Definition pl bl None body (Some ret_type); let evd,rev_pconstants = List.fold_left diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index 56ed406e2f..b32b27ebeb 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -127,13 +127,13 @@ let save id const ?hook uctx scope kind = let fix_exn = Future.fix_exn_of const.Proof_global.proof_entry_body in let r = match scope with | Discharge -> - let k = Kindops.logical_kind_of_goal_kind kind in + let k = Decls.logical_kind_of_goal_kind kind in let c = SectionLocalDef const in let _ = declare_variable id (Lib.cwd(), c, k) in VarRef id | Global local -> - let k = Kindops.logical_kind_of_goal_kind kind in - let kn = declare_constant id ~local (Declare.DefinitionEntry const, k) in + let k = Decls.logical_kind_of_goal_kind kind in + let kn = declare_constant id ~local (DefinitionEntry const, k) in ConstRef kn in DeclareDef.Hook.(call ?hook ~fix_exn { S.uctx; obls = []; scope; dref = r }); diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli index 45d332031f..1758efe584 100644 --- a/plugins/funind/indfun_common.mli +++ b/plugins/funind/indfun_common.mli @@ -48,7 +48,7 @@ val save -> ?hook:DeclareDef.Hook.t -> UState.t -> DeclareDef.locality - -> Decl_kinds.goal_object_kind + -> Decls.goal_object_kind -> unit (* [with_full_print f a] applies [f] to [a] in full printing environment. diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index 86defb2f2f..153b27c855 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -805,7 +805,7 @@ let derive_correctness make_scheme (funs: pconstant list) (graphs:inductive list let (typ,_) = lemmas_types_infos.(i) in let info = Lemmas.Info.make ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior) - ~kind:(Decl_kinds.Proof Decl_kinds.Theorem) () in + ~kind:(Decls.(Proof Theorem)) () in let lemma = Lemmas.start_lemma ~name:lem_id ~poly:false @@ -871,7 +871,7 @@ let derive_correctness make_scheme (funs: pconstant list) (graphs:inductive list let lem_id = mk_complete_id f_id in let info = Lemmas.Info.make ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior) - ~kind:Decl_kinds.(Proof Theorem) () in + ~kind:Decls.(Proof Theorem) () in let lemma = Lemmas.start_lemma ~name:lem_id ~poly:false ~info sigma (fst lemmas_types_infos.(i)) in let lemma = fst (Lemmas.by diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index d38e28c0e7..0398acf242 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -30,7 +30,6 @@ open Tacmach open Tactics open Nametab open Declare -open Decl_kinds open Tacred open Goal open Glob_term @@ -196,7 +195,7 @@ let (value_f: Constr.t list -> GlobRef.t -> Constr.t) = let body = EConstr.Unsafe.to_constr body in it_mkLambda_or_LetIn body context -let (declare_f : Id.t -> logical_kind -> Constr.t list -> GlobRef.t -> GlobRef.t) = +let (declare_f : Id.t -> Decls.logical_kind -> Constr.t list -> GlobRef.t -> GlobRef.t) = fun f_id kind input_type fterm_ref -> declare_fun f_id kind (value_f input_type fterm_ref);; @@ -1368,7 +1367,7 @@ let open_new_goal ~lemma build_proof sigma using_lemmas ref_ goal_name (gls_type Lemmas.save_lemma_proved ~lemma ~opaque:opacity ~idopt:None in let info = Lemmas.Info.make ~hook:(DeclareDef.Hook.make hook) - ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior) ~kind:(Decl_kinds.Proof Decl_kinds.Lemma) + ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior) ~kind:(Decls.(Proof Lemma)) () in let lemma = Lemmas.start_lemma ~name:na @@ -1411,7 +1410,7 @@ let com_terminate nb_args ctx hook = let start_proof env ctx (tac_start:tactic) (tac_end:tactic) = - let info = Lemmas.Info.make ~hook ~scope:(DeclareDef.Global ImportDefaultBehavior) ~kind:(Proof Lemma) () in + let info = Lemmas.Info.make ~hook ~scope:(DeclareDef.Global ImportDefaultBehavior) ~kind:Decls.(Proof Lemma) () in let lemma = Lemmas.start_lemma ~name:thm_name ~poly:false (*FIXME*) ~sign:(Environ.named_context_val env) @@ -1535,7 +1534,7 @@ let recursive_definition ~interactive_proof ~is_mes function_name rec_impls type let term_id = add_suffix function_name "_terminate" in let functional_ref = let univs = Evd.univ_entry ~poly:false evd in - declare_fun functional_id (IsDefinition Decl_kinds.Definition) ~univs res + declare_fun functional_id Decls.(IsDefinition Definition) ~univs res in (* Refresh the global universes, now including those of _F *) let evd = Evd.from_env (Global.env ()) in @@ -1549,7 +1548,7 @@ let recursive_definition ~interactive_proof ~is_mes function_name rec_impls type (* let _ = Pp.msgnl (fun _ _ -> str "relation := " ++ Printer.pr_lconstr_env env_with_pre_rec_args relation) in *) let hook { DeclareDef.Hook.S.uctx ; _ } = let term_ref = Nametab.locate (qualid_of_ident term_id) in - let f_ref = declare_f function_name (IsProof Lemma) arg_types term_ref in + let f_ref = declare_f function_name Decls.(IsProof Lemma) arg_types term_ref in let _ = Extraction_plugin.Table.extraction_inline true [qualid_of_ident term_id] in (* message "start second proof"; *) let stop = diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index 19866df8e3..22ad75b784 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -1901,8 +1901,8 @@ let declare_projection n instance_id r = let cst = Declare.definition_entry ~types:typ ~univs term in - ignore(Declare.declare_constant n - (Declare.DefinitionEntry cst, Decl_kinds.IsDefinition Decl_kinds.Definition)) + ignore(Declare.declare_constant n + (Declare.DefinitionEntry cst, Decls.(IsDefinition Definition))) let build_morphism_signature env sigma m = let m,ctx = Constrintern.interp_constr env sigma m in @@ -1981,7 +1981,7 @@ let add_morphism_as_parameter atts m n : unit = let cst = Declare.declare_constant instance_id (Declare.ParameterEntry (None,(instance,uctx),None), - Decl_kinds.IsAssumption Decl_kinds.Logical) + Decls.(IsAssumption Logical)) in Classes.add_instance (Classes.mk_instance (PropGlobal.proper_class env evd) Hints.empty_hint_info atts.global (ConstRef cst)); @@ -1995,7 +1995,7 @@ let add_morphism_interactive atts m n : Lemmas.t = let evd = Evd.from_env env in let uctx, instance = build_morphism_signature env evd m in let poly = atts.polymorphic in - let kind = Decl_kinds.DefinitionBody Decl_kinds.Instance in + let kind = Decls.(DefinitionBody Instance) in let tac = make_tactic "Coq.Classes.SetoidTactics.add_morphism_tactic" in let hook { DeclareDef.Hook.S.dref; _ } = dref |> function | Globnames.ConstRef cst -> diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml index 33798c43c8..3d6bfda0b2 100644 --- a/plugins/setoid_ring/newring.ml +++ b/plugins/setoid_ring/newring.ml @@ -29,7 +29,6 @@ open Tacinterp open Libobject open Printer open Declare -open Decl_kinds open Entries open Newring_ast open Proofview.Notations @@ -158,7 +157,7 @@ let decl_constant na univs c = let univs = Monomorphic_entry Univ.ContextSet.empty in mkConst(declare_constant (Id.of_string na) (DefinitionEntry (definition_entry ~opaque:true ~types ~univs c), - IsProof Lemma)) + Decls.(IsProof Lemma))) (* Calling a global tactic *) let ltac_call tac (args:glob_tactic_arg list) = diff --git a/tactics/abstract.ml b/tactics/abstract.ml index 662a2fc22c..56f432ee1d 100644 --- a/tactics/abstract.ml +++ b/tactics/abstract.ml @@ -13,7 +13,6 @@ module CVars = Vars open Util open Termops open EConstr -open Decl_kinds open Evarutil module RelDecl = Context.Rel.Declaration @@ -153,7 +152,7 @@ let cache_term_by_tactic_then ~opaque ~name_op ?(goal_type=None) tac tacK = let const, args = shrink_entry sign const in let args = List.map EConstr.of_constr args in let cd = Declare.DefinitionEntry { const with Proof_global.proof_entry_opaque = opaque } in - let decl = (cd, if opaque then IsProof Lemma else IsDefinition Definition) in + let decl = (cd, if opaque then Decls.(IsProof Lemma) else Decls.(IsDefinition Definition)) in let cst () = (* do not compute the implicit arguments, it may be costly *) let () = Impargs.make_implicit_args false in diff --git a/tactics/declare.ml b/tactics/declare.ml index aa94ab5a25..b994585e8a 100644 --- a/tactics/declare.ml +++ b/tactics/declare.ml @@ -24,7 +24,6 @@ open Lib open Impargs open Safe_typing open Cooking -open Decls open Decl_kinds module NamedDecl = Context.Named.Declaration @@ -36,7 +35,7 @@ type import_status = ImportDefaultBehavior | ImportNeedQualified type constant_obj = { cst_decl : Cooking.recipe option; (** Non-empty only when rebuilding a constant after a section *) - cst_kind : logical_kind; + cst_kind : Decls.logical_kind; cst_locl : import_status; } @@ -45,7 +44,7 @@ type 'a constant_entry = | ParameterEntry of parameter_entry | PrimitiveEntry of primitive_entry -type constant_declaration = Evd.side_effects constant_entry * logical_kind +type constant_declaration = Evd.side_effects constant_entry * Decls.logical_kind (* At load-time, the segment starting from the module name to the discharge *) (* section (if Remark or Fact) is needed to access a construction *) @@ -54,7 +53,7 @@ let load_constant i ((sp,kn), obj) = alreadydeclared (Id.print (basename sp) ++ str " already exists"); let con = Global.constant_of_delta_kn kn in Nametab.push (Nametab.Until i) sp (ConstRef con); - add_constant_kind con obj.cst_kind + Decls.add_constant_kind con obj.cst_kind let cooking_info segment = let modlist = replacement_context () in @@ -73,7 +72,7 @@ let open_constant i ((sp,kn), obj) = Nametab.push (Nametab.Exactly i) sp (ConstRef con) let exists_name id = - variable_exists id || Global.exists_objlabel (Label.of_id id) + Decls.variable_exists id || Global.exists_objlabel (Label.of_id id) let check_exists id = if exists_name id then alreadydeclared (Id.print id ++ str " already exists") @@ -95,7 +94,7 @@ let cache_constant ((sp,kn), obj) = Nametab.push (Nametab.Until 1) sp (ConstRef (Constant.make1 kn)); let cst = Global.lookup_constant kn' in add_section_constant ~poly:(Declareops.constant_is_polymorphic cst) kn' cst.const_hyps; - add_constant_kind (Constant.make1 kn) obj.cst_kind + Decls.add_constant_kind (Constant.make1 kn) obj.cst_kind let discharge_constant ((sp, kn), obj) = let con = Constant.make1 kn in @@ -141,7 +140,7 @@ let register_constant kn kind local = update_tables kn let register_side_effect (c, role) = - let () = register_constant c (IsProof Theorem) ImportDefaultBehavior in + let () = register_constant c Decls.(IsProof Theorem) ImportDefaultBehavior in match role with | None -> () | Some (Evd.Schema (ind, kind)) -> !declare_scheme kind [|ind,c|] @@ -294,27 +293,27 @@ let declare_private_constant ?role ?(local = ImportDefaultBehavior) id (cd, kind kn, eff let declare_definition - ?(opaque=false) ?(kind=Decl_kinds.Definition) ?(local = ImportDefaultBehavior) + ?(opaque=false) ?(kind=Decls.Definition) ?(local = ImportDefaultBehavior) id ?types (body,univs) = let cb = definition_entry ?types ~univs ~opaque body in declare_constant ~local id - (DefinitionEntry cb, Decl_kinds.IsDefinition kind) + (DefinitionEntry cb, Decls.IsDefinition kind) (** Declaration of section variables and local definitions *) type section_variable_entry = | SectionLocalDef of Evd.side_effects Proof_global.proof_entry | SectionLocalAssum of { typ:types; univs:Univ.ContextSet.t; poly:bool; impl:bool } -type variable_declaration = DirPath.t * section_variable_entry * logical_kind +type variable_declaration = DirPath.t * section_variable_entry * Decls.logical_kind let cache_variable ((sp,_),o) = match o with | Inl ctx -> Global.push_context_set false ctx | Inr (id,(path,d,kind)) -> (* Constr raisonne sur les noms courts *) - if variable_exists id then + if Decls.variable_exists id then alreadydeclared (Id.print id ++ str " already exists"); let impl,opaque,poly,univs = match d with (* Fails if not well-typed *) @@ -349,12 +348,12 @@ let cache_variable ((sp,_),o) = poly, univs in Nametab.push (Nametab.Until 1) (restrict_path 0 sp) (VarRef id); add_section_variable ~name:id ~kind:impl ~poly univs; - add_variable_data id {path;opaque;univs;poly;kind} + Decls.(add_variable_data id {path;opaque;univs;poly;kind}) let discharge_variable (_,o) = match o with | Inr (id,_) -> - if variable_polymorphic id then None - else Some (Inl (variable_context id)) + if Decls.variable_polymorphic id then None + else Some (Inl (Decls.variable_context id)) | Inl _ -> Some o type variable_obj = @@ -491,11 +490,10 @@ let declare_one_projection univs (mind,_ as ind) ~proj_npars proj_arg label (ter let term = Vars.subst_instance_constr u term in let types = Vars.subst_instance_constr u types in let entry = definition_entry ~types ~univs term in - let cst = declare_constant id (DefinitionEntry entry, IsDefinition StructureComponent) in + let cst = declare_constant id (DefinitionEntry entry, Decls.(IsDefinition StructureComponent)) in let p = Projection.Repr.make ind ~proj_npars ~proj_arg label in declare_primitive_projection p cst - let declare_projections univs mind = let env = Global.env () in let mib = Environ.lookup_mind mind env in diff --git a/tactics/declare.mli b/tactics/declare.mli index 1f72fff30e..0fc22f26c4 100644 --- a/tactics/declare.mli +++ b/tactics/declare.mli @@ -11,7 +11,6 @@ open Names open Constr open Entries -open Decl_kinds (** This module provides the official functions to declare new variables, parameters, constants and inductive types. Using the following functions @@ -31,14 +30,14 @@ type 'a constant_entry = | ParameterEntry of parameter_entry | PrimitiveEntry of primitive_entry -type variable_declaration = DirPath.t * section_variable_entry * logical_kind +type variable_declaration = DirPath.t * section_variable_entry * Decls.logical_kind val declare_variable : variable -> variable_declaration -> Libobject.object_name (** Declaration of global constructions i.e. Definition/Theorem/Axiom/Parameter/... *) -type constant_declaration = Evd.side_effects constant_entry * logical_kind +type constant_declaration = Evd.side_effects constant_entry * Decls.logical_kind (* Default definition entries, transparent with no secctx or proj information *) val definition_entry : ?fix_exn:Future.fix_exn -> @@ -61,7 +60,7 @@ val declare_private_constant : ?role:Evd.side_effect_role -> ?local:import_status -> Id.t -> constant_declaration -> Constant.t * Evd.side_effects val declare_definition : - ?opaque:bool -> ?kind:definition_object_kind -> + ?opaque:bool -> ?kind:Decls.definition_object_kind -> ?local:import_status -> Id.t -> ?types:constr -> constr Entries.in_universes_entry -> Constant.t diff --git a/tactics/ind_tables.ml b/tactics/ind_tables.ml index e01f3ab961..29963bc105 100644 --- a/tactics/ind_tables.ml +++ b/tactics/ind_tables.ml @@ -22,7 +22,6 @@ open Declarations open Constr open CErrors open Util -open Decl_kinds open Pp (**********************************************************************) @@ -136,7 +135,7 @@ let define internal role id c poly univs = proof_entry_inline_code = false; proof_entry_feedback = None; } in - let kn, eff = Declare.declare_private_constant ~role id (Declare.DefinitionEntry entry, Decl_kinds.IsDefinition Scheme) in + let kn, eff = Declare.declare_private_constant ~role id (Declare.DefinitionEntry entry, Decls.(IsDefinition Scheme)) in let () = match internal with | InternalTacticRequest -> () | _-> Declare.definition_message id diff --git a/tactics/leminv.ml b/tactics/leminv.ml index e242b10d33..2ef06d2246 100644 --- a/tactics/leminv.ml +++ b/tactics/leminv.ml @@ -27,7 +27,6 @@ open Tacmach.New open Clenv open Tacticals.New open Tactics -open Decl_kinds open Context.Named.Declaration module NamedDecl = Context.Named.Declaration @@ -236,7 +235,7 @@ let add_inversion_lemma ~poly name env sigma t sort dep inv_op = let invProof, sigma = inversion_scheme ~name ~poly env sigma t sort dep inv_op in let univs = Evd.univ_entry ~poly sigma in let entry = Declare.definition_entry ~univs invProof in - let _ = Declare.declare_constant name (Declare.DefinitionEntry entry, IsProof Lemma) in + let _ = Declare.declare_constant name (Declare.DefinitionEntry entry, Decls.(IsProof Lemma)) in () (* inv_op = Inv (derives de complete inv. lemma) diff --git a/vernac/class.ml b/vernac/class.ml index 6dba134764..c0d8837c2e 100644 --- a/vernac/class.ml +++ b/vernac/class.ml @@ -21,7 +21,6 @@ open Environ open Classops open Declare open Globnames -open Decl_kinds open Libobject let strength_min l = if List.mem `LOCAL l then `LOCAL else `GLOBAL @@ -222,7 +221,7 @@ let build_id_coercion idf_opt source poly = (definition_entry ~types:typ_f ~univs ~inline:true (mkCast (val_f, DEFAULTcast, typ_f))) in - let decl = (constr_entry, IsDefinition IdentityCoercion) in + let decl = (constr_entry, Decls.(IsDefinition IdentityCoercion)) in let kn = declare_constant idf decl in ConstRef kn diff --git a/vernac/classes.ml b/vernac/classes.ml index fbcd1744a8..01fc120af2 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -315,7 +315,7 @@ let instance_hook info global imps ?hook cst = let declare_instance_constant info global imps ?hook id decl poly sigma term termtype = (* XXX: Duplication of the declare_constant path *) - let kind = IsDefinition Instance in + let kind = Decls.(IsDefinition Instance) in let sigma = let levels = Univ.LSet.union (CVars.universes_of_constr termtype) (CVars.universes_of_constr term) in @@ -338,7 +338,7 @@ let do_declare_instance sigma ~global ~poly k u ctx ctx' pri decl imps subst id let termtype = it_mkProd_or_LetIn ty_constr (ctx' @ ctx) in let sigma, entry = DeclareDef.prepare_parameter ~allow_evars:false ~poly sigma decl termtype in let cst = Declare.declare_constant id - (Declare.ParameterEntry entry, Decl_kinds.IsAssumption Decl_kinds.Logical) in + (Declare.ParameterEntry entry, Decls.(IsAssumption Logical)) in Declare.declare_univ_binders (ConstRef cst) (Evd.universe_binders sigma); instance_hook pri global imps (ConstRef cst) @@ -363,7 +363,7 @@ let declare_instance_program env sigma ~global ~poly id pri imps decl term termt let hook = DeclareDef.Hook.make hook in let ctx = Evd.evar_universe_context sigma in ignore(Obligations.add_definition ~name:id ?term:constr - ~univdecl:decl ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior) ~poly ~kind:Instance ~hook typ ctx obls) + ~univdecl:decl ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior) ~poly ~kind:Decls.Instance ~hook typ ctx obls) let declare_instance_open sigma ?hook ~tac ~global ~poly id pri imps udecl ids term termtype = (* spiwack: it is hard to reorder the actions to do @@ -373,7 +373,7 @@ let declare_instance_open sigma ?hook ~tac ~global ~poly id pri imps udecl ids t let gls = List.rev (Evd.future_goals sigma) in let sigma = Evd.reset_future_goals sigma in let scope = DeclareDef.Global Declare.ImportDefaultBehavior in - let kind = Decl_kinds.DefinitionBody Decl_kinds.Instance in + let kind = Decls.(DefinitionBody Instance) in let hook = DeclareDef.Hook.(make (fun { S.dref ; _ } -> instance_hook pri global imps ?hook dref)) in let info = Lemmas.Info.make ~hook ~scope ~kind () in let lemma = Lemmas.start_lemma ~name:id ~poly ~udecl ~info sigma (EConstr.of_constr termtype) in diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml index e91d8b9d3e..d7ad5133a6 100644 --- a/vernac/comAssumption.ml +++ b/vernac/comAssumption.ml @@ -18,7 +18,6 @@ open Globnames open Constrexpr_ops open Constrintern open Impargs -open Decl_kinds open Pretyping open Entries @@ -36,7 +35,7 @@ let () = optread = (fun _ -> !axiom_into_instance); optwrite = (:=) axiom_into_instance; } -let should_axiom_into_instance = function +let should_axiom_into_instance = let open Decls in function | Context -> (* The typeclass behaviour of Variable and Context doesn't depend on section status *) @@ -51,7 +50,7 @@ match scope with | Monomorphic_entry univs -> univs | Polymorphic_entry (_, univs) -> Univ.ContextSet.of_context univs in - let decl = (Lib.cwd(), SectionLocalAssum {typ;univs;poly;impl}, IsAssumption kind) in + let decl = (Lib.cwd(), SectionLocalAssum {typ;univs;poly;impl}, Decls.IsAssumption kind) in let _ = declare_variable ident decl in let () = assumption_message ident in let r = VarRef ident in @@ -69,7 +68,7 @@ match scope with | DefaultInline -> Some (Flags.get_inline_level()) | InlineAt i -> Some i in - let decl = (Declare.ParameterEntry (None,(typ,univs),inl), IsAssumption kind) in + let decl = (Declare.ParameterEntry (None,(typ,univs),inl), Decls.IsAssumption kind) in let kn = declare_constant ident ~local decl in let gr = ConstRef kn in let () = maybe_declare_manual_implicits false gr imps in @@ -211,7 +210,7 @@ let do_primitive id prim typopt = prim_entry_content = prim; } in - let _kn = declare_constant id.CAst.v (PrimitiveEntry entry,IsPrimitive) in + let _kn = declare_constant id.CAst.v (PrimitiveEntry entry, Decls.IsPrimitive) in Flags.if_verbose Feedback.msg_info Pp.(Id.print id.CAst.v ++ str " is declared") let named_of_rel_context l = @@ -275,10 +274,10 @@ let context ~poly l = (* Declare the universe context once *) let decl = match b with | None -> - (Declare.ParameterEntry (None,(t,univs),None), IsAssumption Logical) + (Declare.ParameterEntry (None,(t,univs),None), Decls.(IsAssumption Logical)) | Some b -> let entry = Declare.definition_entry ~univs ~types:t b in - (Declare.DefinitionEntry entry, IsAssumption Logical) + (Declare.DefinitionEntry entry, Decls.(IsAssumption Logical)) in let cst = Declare.declare_constant id decl in let env = Global.env () in @@ -294,13 +293,13 @@ let context ~poly l = if Lib.sections_are_opened () then DeclareDef.Discharge else DeclareDef.Global ImportDefaultBehavior in let nstatus = match b with | None -> - pi3 (declare_assumption false ~scope ~poly ~kind:Context t univs UnivNames.empty_binders [] impl + pi3 (declare_assumption false ~scope ~poly ~kind:Decls.Context t univs UnivNames.empty_binders [] impl Declaremods.NoInline (CAst.make id)) | Some b -> let entry = Declare.definition_entry ~univs ~types:t b in let _gr = DeclareDef.declare_definition ~name:id ~scope:DeclareDef.Discharge - ~kind:Definition UnivNames.empty_binders entry [] in + ~kind:Decls.Definition UnivNames.empty_binders entry [] in Lib.sections_are_opened () || Lib.is_modtype_strict () in status && nstatus diff --git a/vernac/comAssumption.mli b/vernac/comAssumption.mli index 57b4aea9e3..028ed39656 100644 --- a/vernac/comAssumption.mli +++ b/vernac/comAssumption.mli @@ -11,7 +11,6 @@ open Names open Vernacexpr open Constrexpr -open Decl_kinds (** {6 Parameters/Assumptions} *) @@ -19,7 +18,7 @@ val do_assumptions : program_mode:bool -> poly:bool -> scope:DeclareDef.locality - -> kind:assumption_object_kind + -> kind:Decls.assumption_object_kind -> Declaremods.inline -> (ident_decl list * constr_expr) with_coercion list -> bool @@ -30,7 +29,7 @@ val declare_assumption : coercion_flag -> poly:bool -> scope:DeclareDef.locality - -> kind:assumption_object_kind + -> kind:Decls.assumption_object_kind -> Constr.types -> Entries.universes_entry -> UnivNames.universe_binders diff --git a/vernac/comDefinition.mli b/vernac/comDefinition.mli index 71926a9d23..db0c102e14 100644 --- a/vernac/comDefinition.mli +++ b/vernac/comDefinition.mli @@ -9,7 +9,6 @@ (************************************************************************) open Names -open Decl_kinds open Redexpr open Constrexpr @@ -21,7 +20,7 @@ val do_definition -> name:Id.t -> scope:DeclareDef.locality -> poly:bool - -> kind:definition_object_kind + -> kind:Decls.definition_object_kind -> universe_decl_expr option -> local_binder_expr list -> red_expr option diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml index e3428d6afc..cc2f7d9f70 100644 --- a/vernac/comFixpoint.ml +++ b/vernac/comFixpoint.ml @@ -20,7 +20,6 @@ open Names open Constrexpr open Constrexpr_ops open Constrintern -open Decl_kinds open Pretyping open Evarutil open Evarconv @@ -257,8 +256,8 @@ let interp_fixpoint ~cofix l ntns = let declare_fixpoint_interactive_generic ?indexes ~scope ~poly ((fixnames,_fixrs,fixdefs,fixtypes),udecl,ctx,fiximps) ntns = let fix_kind, cofix, indexes = match indexes with - | Some indexes -> Fixpoint, false, indexes - | None -> CoFixpoint, true, [] + | Some indexes -> Decls.Fixpoint, false, indexes + | None -> Decls.CoFixpoint, true, [] in let thms = List.map3 (fun name t (ctx,impargs,_) -> @@ -269,7 +268,7 @@ let declare_fixpoint_interactive_generic ?indexes ~scope ~poly ((fixnames,_fixrs Some (List.map (Option.cata (EConstr.of_constr %> Tactics.exact_no_check) Tacticals.New.tclIDTAC) fixdefs) in let evd = Evd.from_ctx ctx in let lemma = - Lemmas.start_lemma_with_initialization ~poly ~scope ~kind:(DefinitionBody fix_kind) ~udecl + Lemmas.start_lemma_with_initialization ~poly ~scope ~kind:(Decls.DefinitionBody fix_kind) ~udecl evd (Some(cofix,indexes,init_tac)) thms None in (* Declare notations *) List.iter (Metasyntax.add_notation_interpretation (Global.env())) ntns; @@ -278,8 +277,8 @@ let declare_fixpoint_interactive_generic ?indexes ~scope ~poly ((fixnames,_fixrs let declare_fixpoint_generic ?indexes ~scope ~poly ((fixnames,fixrs,fixdefs,fixtypes),pl,ctx,fiximps) ntns = let indexes, cofix, fix_kind = match indexes with - | Some indexes -> indexes, false, Fixpoint - | None -> [], true, CoFixpoint + | Some indexes -> indexes, false, Decls.Fixpoint + | None -> [], true, Decls.CoFixpoint in (* We shortcut the proof process *) let fixdefs = List.map Option.get fixdefs in diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml index 3947bb1b14..95f8fff520 100644 --- a/vernac/comProgramFixpoint.ml +++ b/vernac/comProgramFixpoint.ml @@ -22,7 +22,6 @@ open Nameops open Constrexpr open Constrexpr_ops open Constrintern -open Decl_kinds open Evarutil open Context.Rel.Declaration open ComFixpoint @@ -213,7 +212,7 @@ let build_wellfounded (recname,pl,bl,arityc,body) poly r measure notation = (*FIXME poly? *) let ce = definition_entry ~types:ty ~univs (EConstr.to_constr sigma body) in (* FIXME: include locality *) - let c = Declare.declare_constant recname (DefinitionEntry ce, IsDefinition Definition) in + let c = Declare.declare_constant recname (DefinitionEntry ce, Decls.(IsDefinition Definition)) in let gr = ConstRef c in if Impargs.is_implicit_args () || not (List.is_empty impls) then Impargs.declare_manual_implicits false gr impls @@ -288,8 +287,8 @@ let do_program_recursive ~scope ~poly fixkind fixl ntns = end in let ctx = Evd.evar_universe_context evd in let kind = match fixkind with - | DeclareObl.IsFixpoint _ -> Fixpoint - | DeclareObl.IsCoFixpoint -> CoFixpoint + | DeclareObl.IsFixpoint _ -> Decls.Fixpoint + | DeclareObl.IsCoFixpoint -> Decls.CoFixpoint in Obligations.add_mutual_definitions defs ~poly ~scope ~kind ~univdecl:pl ctx ntns fixkind diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml index d229973936..7487c99f56 100644 --- a/vernac/declareDef.ml +++ b/vernac/declareDef.ml @@ -8,7 +8,6 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -open Decl_kinds open Declare open Globnames open Impargs @@ -49,10 +48,10 @@ let declare_definition ~name ~scope ~kind ?hook_data udecl ce imps = let fix_exn = Future.fix_exn_of ce.Proof_global.proof_entry_body in let gr = match scope with | Discharge -> - let _ = declare_variable name (Lib.cwd(), SectionLocalDef ce, IsDefinition kind) in + let _ = declare_variable name (Lib.cwd(), SectionLocalDef ce, Decls.IsDefinition kind) in VarRef name | Global local -> - let kn = declare_constant name ~local (DefinitionEntry ce, IsDefinition kind) in + let kn = declare_constant name ~local (DefinitionEntry ce, Decls.IsDefinition kind) in let gr = ConstRef kn in let () = Declare.declare_univ_binders gr udecl in gr diff --git a/vernac/declareDef.mli b/vernac/declareDef.mli index cfff89bc34..606cfade46 100644 --- a/vernac/declareDef.mli +++ b/vernac/declareDef.mli @@ -9,7 +9,6 @@ (************************************************************************) open Names -open Decl_kinds type locality = Discharge | Global of Declare.import_status @@ -43,7 +42,7 @@ end val declare_definition : name:Id.t -> scope:locality - -> kind:definition_object_kind + -> kind:Decls.definition_object_kind -> ?hook_data:(Hook.t * UState.t * (Id.t * Constr.t) list) -> UnivNames.universe_binders -> Evd.side_effects Proof_global.proof_entry @@ -55,7 +54,7 @@ val declare_fix -> ?hook_data:(Hook.t * UState.t * (Id.t * Constr.t) list) -> name:Id.t -> scope:locality - -> kind:definition_object_kind + -> kind:Decls.definition_object_kind -> UnivNames.universe_binders -> Entries.universes_entry -> Evd.side_effects Entries.proof_output diff --git a/vernac/declareObl.ml b/vernac/declareObl.ml index cd521255a0..0ab02862f0 100644 --- a/vernac/declareObl.ml +++ b/vernac/declareObl.ml @@ -14,7 +14,6 @@ open Environ open Context open Constr open Vars -open Decl_kinds open Entries type 'a obligation_body = DefinedObl of 'a | TermObl of constr @@ -50,7 +49,7 @@ type program_info = ; prg_notations : notations ; prg_poly : bool ; prg_scope : DeclareDef.locality - ; prg_kind : definition_object_kind + ; prg_kind : Decls.definition_object_kind ; prg_reduce : constr -> constr ; prg_hook : DeclareDef.Hook.t option ; prg_opaque : bool @@ -168,7 +167,7 @@ let declare_obligation prg obl body ty uctx = (* ppedrot: seems legit to have obligations as local *) let constant = Declare.declare_constant obl.obl_name ~local:Declare.ImportNeedQualified - (Declare.DefinitionEntry ce, IsProof Property) + (Declare.DefinitionEntry ce, Decls.(IsProof Property)) in if not opaque then add_hint (Locality.make_section_locality None) prg constant; @@ -423,7 +422,7 @@ let declare_mutual_definition l = let fixdecls = (Array.map2 make_annot namevec rvec, arrrec, recvec) in let fixnames = first.prg_deps in let opaque = first.prg_opaque in - let kind = if fixkind != IsCoFixpoint then Fixpoint else CoFixpoint in + let kind = if fixkind != IsCoFixpoint then Decls.Fixpoint else Decls.CoFixpoint in let indexes, fixdecls = match fixkind with | IsFixpoint wfl -> diff --git a/vernac/declareObl.mli b/vernac/declareObl.mli index fae27e1cb3..7433888cec 100644 --- a/vernac/declareObl.mli +++ b/vernac/declareObl.mli @@ -44,7 +44,7 @@ type program_info = ; prg_notations : notations ; prg_poly : bool ; prg_scope : DeclareDef.locality - ; prg_kind : Decl_kinds.definition_object_kind + ; prg_kind : Decls.definition_object_kind ; prg_reduce : constr -> constr ; prg_hook : DeclareDef.Hook.t option ; prg_opaque : bool diff --git a/vernac/g_proofs.mlg b/vernac/g_proofs.mlg index 94876d2142..5cffa18511 100644 --- a/vernac/g_proofs.mlg +++ b/vernac/g_proofs.mlg @@ -55,7 +55,7 @@ GRAMMAR EXTEND Gram ; command: [ [ IDENT "Goal"; c = lconstr -> - { VernacDefinition (Decl_kinds.(NoDischarge, Definition), ((CAst.make ~loc Names.Anonymous), None), ProveBody ([], c)) } + { VernacDefinition (Decls.(NoDischarge, Definition), ((CAst.make ~loc Names.Anonymous), None), ProveBody ([], c)) } | IDENT "Proof" -> { VernacProof (None,None) } | IDENT "Proof" ; IDENT "Mode" ; mn = string -> { VernacProofMode mn } | IDENT "Proof"; c = lconstr -> { VernacExactProof c } diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg index 74bd552459..2b475f1ef9 100644 --- a/vernac/g_vernac.mlg +++ b/vernac/g_vernac.mlg @@ -20,7 +20,7 @@ open Impargs open Constrexpr open Constrexpr_ops open Extend -open Decl_kinds +open Decls open Declaremods open Declarations open Namegen diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml index 9559edbea0..26499ce994 100644 --- a/vernac/indschemes.ml +++ b/vernac/indschemes.ml @@ -24,7 +24,6 @@ open Declarations open Term open Constr open Inductive -open Decl_kinds open Indrec open Declare open Libnames @@ -114,7 +113,7 @@ let define ~poly id sigma c t = proof_entry_inline_code = false; proof_entry_feedback = None; }, - Decl_kinds.IsDefinition Scheme) in + Decls.(IsDefinition Scheme)) in definition_message id; kn diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index e586200ba3..2908481dea 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -22,7 +22,6 @@ open Entries open Nameops open Globnames open Decls -open Decl_kinds open Declare open Pretyping open Termops @@ -75,7 +74,7 @@ module Info = struct (* This could be improved and the CEphemeron removed *) ; other_thms : Recthm.t list ; scope : DeclareDef.locality - ; kind : Decl_kinds.goal_object_kind + ; kind : Decls.goal_object_kind } let make ?hook ?(proof_ending=Proof_ending.Regular) ?(scope=DeclareDef.Global Declare.ImportDefaultBehavior) ?(kind=Proof Lemma) () = @@ -497,7 +496,7 @@ let finish_proved env sigma idopt po info = let fix_exn = Future.fix_exn_of const.proof_entry_body in let () = try let const = adjust_guardness_conditions const compute_guard in - let k = Kindops.logical_kind_of_goal_kind kind in + let k = Decls.logical_kind_of_goal_kind kind in let should_suggest = const.proof_entry_opaque && Option.is_empty const.proof_entry_secctx in let open DeclareDef in let r = match scope with @@ -543,7 +542,7 @@ let finish_derived ~f ~name ~idopt ~entries = (* The opacity of [f_def] is adjusted to be [false], as it must. Then [f] is declared in the global environment. *) let f_def = { f_def with Proof_global.proof_entry_opaque = false } in - let f_def = Declare.DefinitionEntry f_def , Decl_kinds.(IsDefinition Definition) in + let f_def = Declare.DefinitionEntry f_def , IsDefinition Definition in let f_kn = Declare.declare_constant f f_def in let f_kn_term = mkConst f_kn in (* In the type and body of the proof of [suchthat] there can be @@ -568,14 +567,13 @@ let finish_derived ~f ~name ~idopt ~entries = in let lemma_def = Declare.DefinitionEntry lemma_def , - Decl_kinds.(IsProof Proposition) + Decls.(IsProof Proposition) in let _ : Names.Constant.t = Declare.declare_constant name lemma_def in () let finish_proved_equations lid kind proof_obj hook i types wits sigma0 = - let open Decl_kinds in let obls = ref 1 in let kind = match kind with | DefinitionBody d -> IsDefinition d diff --git a/vernac/lemmas.mli b/vernac/lemmas.mli index d156954c85..39c074d4ff 100644 --- a/vernac/lemmas.mli +++ b/vernac/lemmas.mli @@ -9,7 +9,6 @@ (************************************************************************) open Names -open Decl_kinds (** {4 Proofs attached to a constant} *) @@ -68,7 +67,7 @@ module Info : sig (** Info for special constants *) -> ?scope : DeclareDef.locality (** locality *) - -> ?kind:goal_object_kind + -> ?kind:Decls.goal_object_kind (** Theorem, etc... *) -> unit -> t @@ -101,7 +100,7 @@ val start_lemma_with_initialization : ?hook:DeclareDef.Hook.t -> poly:bool -> scope:DeclareDef.locality - -> kind:goal_object_kind + -> kind:Decls.goal_object_kind -> udecl:UState.universe_decl -> Evd.evar_map -> (bool * lemma_possible_guards * unit Proofview.tactic list option) option @@ -116,7 +115,7 @@ val start_lemma_com : program_mode:bool -> poly:bool -> scope:DeclareDef.locality - -> kind:goal_object_kind + -> kind:Decls.goal_object_kind -> ?inference_hook:Pretyping.inference_hook -> ?hook:DeclareDef.Hook.t -> Vernacexpr.proof_expr list diff --git a/vernac/obligations.ml b/vernac/obligations.ml index e82694b740..92adad2299 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -9,7 +9,6 @@ (************************************************************************) open Printf -open Decl_kinds (** - Get types of existentials ; @@ -398,8 +397,8 @@ let deps_remaining obls deps = deps [] -let goal_kind = DeclareDef.(Global Declare.ImportNeedQualified, DefinitionBody Definition) -let goal_proof_kind = DeclareDef.(Global Declare.ImportNeedQualified, Proof Lemma) +let goal_kind = DeclareDef.(Global Declare.ImportNeedQualified, Decls.(DefinitionBody Definition)) +let goal_proof_kind = DeclareDef.(Global Declare.ImportNeedQualified, Decls.(Proof Lemma)) let kind_of_obligation o = match o with @@ -638,7 +637,7 @@ let show_term n = ++ Printer.pr_constr_env env sigma prg.prg_body) let add_definition ~name ?term t ctx ?(univdecl=UState.default_univ_decl) - ?(implicits=[]) ~poly ?(scope=DeclareDef.Global Declare.ImportDefaultBehavior) ?(kind=Definition) ?tactic + ?(implicits=[]) ~poly ?(scope=DeclareDef.Global Declare.ImportDefaultBehavior) ?(kind=Decls.Definition) ?tactic ?(reduce=reduce) ?hook ?(opaque = false) obls = let sign = Lemmas.initialize_named_context_for_proof () in let info = Id.print name ++ str " has type-checked" in @@ -658,7 +657,7 @@ let add_definition ~name ?term t ctx ?(univdecl=UState.default_univ_decl) | _ -> res) let add_mutual_definitions l ctx ?(univdecl=UState.default_univ_decl) ?tactic - ~poly ?(scope=DeclareDef.Global Declare.ImportDefaultBehavior) ?(kind=Definition) ?(reduce=reduce) + ~poly ?(scope=DeclareDef.Global Declare.ImportDefaultBehavior) ?(kind=Decls.Definition) ?(reduce=reduce) ?hook ?(opaque = false) notations fixkind = let sign = Lemmas.initialize_named_context_for_proof () in let deps = List.map (fun (n, b, t, imps, obls) -> n) l in @@ -690,7 +689,7 @@ let admit_prog prg = let x = subst_deps_obl obls x in let ctx = UState.univ_entry ~poly:false prg.prg_ctx in let kn = Declare.declare_constant x.obl_name ~local:Declare.ImportNeedQualified - (Declare.ParameterEntry (None,(x.obl_type,ctx),None), IsAssumption Conjectural) + (Declare.ParameterEntry (None,(x.obl_type,ctx),None), Decls.(IsAssumption Conjectural)) in assumption_message x.obl_name; obls.(i) <- { x with obl_body = Some (DefinedObl (kn, Univ.Instance.empty)) } diff --git a/vernac/obligations.mli b/vernac/obligations.mli index 233739ee46..f97bc784c3 100644 --- a/vernac/obligations.mli +++ b/vernac/obligations.mli @@ -50,7 +50,7 @@ val add_definition -> ?implicits:Impargs.manual_implicits -> poly:bool -> ?scope:DeclareDef.locality - -> ?kind:Decl_kinds.definition_object_kind + -> ?kind:Decls.definition_object_kind -> ?tactic:unit Proofview.tactic -> ?reduce:(constr -> constr) -> ?hook:DeclareDef.Hook.t @@ -66,7 +66,7 @@ val add_mutual_definitions -> ?tactic:unit Proofview.tactic -> poly:bool -> ?scope:DeclareDef.locality - -> ?kind:Decl_kinds.definition_object_kind + -> ?kind:Decls.definition_object_kind -> ?reduce:(constr -> constr) -> ?hook:DeclareDef.Hook.t -> ?opaque:bool -> DeclareObl.notations diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml index 4f053b98ae..78112d9dc4 100644 --- a/vernac/ppvernac.ml +++ b/vernac/ppvernac.ml @@ -16,7 +16,6 @@ open Util open CAst open Extend -open Decl_kinds open Constrexpr open Constrexpr_ops open Vernacexpr @@ -348,18 +347,18 @@ open Pputils let pr_assumption_token many discharge kind = match discharge, kind with - | (NoDischarge,Logical) -> + | (NoDischarge,Decls.Logical) -> keyword (if many then "Axioms" else "Axiom") - | (NoDischarge,Definitional) -> + | (NoDischarge,Decls.Definitional) -> keyword (if many then "Parameters" else "Parameter") - | (NoDischarge,Conjectural) -> str"Conjecture" - | (DoDischarge,Logical) -> + | (NoDischarge,Decls.Conjectural) -> str"Conjecture" + | (DoDischarge,Decls.Logical) -> keyword (if many then "Hypotheses" else "Hypothesis") - | (DoDischarge,Definitional) -> + | (DoDischarge,Decls.Definitional) -> keyword (if many then "Variables" else "Variable") - | (DoDischarge,Conjectural) -> + | (DoDischarge,Decls.Conjectural) -> anomaly (Pp.str "Don't know how to beautify a local conjecture.") - | (_,Context) -> + | (_,Decls.Context) -> anomaly (Pp.str "Context is used only internally.") let pr_params pr_c (xl,(c,t)) = @@ -388,7 +387,16 @@ open Pputils prlist_with_sep pr_semicolon (pr_params pr_c) *) - let pr_thm_token k = keyword (Kindops.string_of_theorem_kind k) +let string_of_theorem_kind = let open Decls in function + | Theorem -> "Theorem" + | Lemma -> "Lemma" + | Fact -> "Fact" + | Remark -> "Remark" + | Property -> "Property" + | Proposition -> "Proposition" + | Corollary -> "Corollary" + + let pr_thm_token k = keyword (string_of_theorem_kind k) let pr_syntax_modifier = let open Gramlib.Gramext in function | SetItemLevel (l,bko,n) -> @@ -588,6 +596,18 @@ open Pputils with Not_found -> hov 1 (str "TODO(" ++ str (fst s) ++ spc () ++ prlist_with_sep sep pr_arg cl ++ str ")") + +let string_of_definition_object_kind = let open Decls in function + | Definition -> "Definition" + | Example -> "Example" + | Coercion -> "Coercion" + | SubClass -> "SubClass" + | CanonicalStructure -> "Canonical Structure" + | Instance -> "Instance" + | Let -> "Let" + | (StructureComponent|Scheme|CoFixpoint|Fixpoint|IdentityCoercion|Method) -> + CErrors.anomaly (Pp.str "Internal definition kind.") + let pr_vernac_expr v = let return = tag_vernac v in let env = Global.env () in @@ -719,7 +739,7 @@ open Pputils keyword ( if Name.is_anonymous (fst id).v then "Goal" - else Kindops.string_of_definition_object_kind dk) + else string_of_definition_object_kind dk) in let pr_reduce = function | None -> mt() diff --git a/vernac/record.ml b/vernac/record.ml index cc4f02349d..08239eb544 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -24,7 +24,6 @@ open Declarations open Entries open Declare open Constrintern -open Decl_kinds open Type_errors open Constrexpr open Constrexpr_ops @@ -282,7 +281,7 @@ type projection_flags = { } (* We build projections *) -let declare_projections indsp ctx ?(kind=StructureComponent) binder_name flags fieldimpls fields = +let declare_projections indsp ctx ?(kind=Decls.StructureComponent) binder_name flags fieldimpls fields = let env = Global.env() in let (mib,mip) = Global.lookup_inductive indsp in let poly = Declareops.inductive_is_polymorphic mib in @@ -352,7 +351,7 @@ let declare_projections indsp ctx ?(kind=StructureComponent) binder_name flags f proof_entry_opaque = false; proof_entry_inline_code = false; proof_entry_feedback = None } in - let k = (Declare.DefinitionEntry entry,IsDefinition kind) in + let k = (Declare.DefinitionEntry entry,Decls.IsDefinition kind) in let kn = declare_constant fid k in let constr_fip = let proj_args = (*Rel 1 refers to "x"*) paramargs@[mkRel 1] in @@ -402,7 +401,7 @@ let inStruc : Recordops.struc_tuple -> obj = let declare_structure_entry o = Lib.add_anonymous_leaf (inStruc o) -let declare_structure ~cum finite ubinders univs paramimpls params template ?(kind=StructureComponent) ?name record_data = +let declare_structure ~cum finite ubinders univs paramimpls params template ?(kind=Decls.StructureComponent) ?name record_data = let nparams = List.length params in let poly, ctx = match univs with @@ -481,7 +480,7 @@ let implicits_of_context ctx = (List.rev (Anonymous :: (List.map RelDecl.get_name ctx))) let declare_class def cum ubinders univs id idbuild paramimpls params arity - template fieldimpls fields ?(kind=StructureComponent) coers priorities = + template fieldimpls fields ?(kind=Decls.StructureComponent) coers priorities = let fieldimpls = (* Make the class implicit in the projections, and the params if applicable. *) let impls = implicits_of_context params in @@ -498,7 +497,7 @@ let declare_class def cum ubinders univs id idbuild paramimpls params arity let class_entry = Declare.definition_entry ~types:class_type ~univs class_body in let cst = Declare.declare_constant id - (DefinitionEntry class_entry, IsDefinition Definition) + (DefinitionEntry class_entry, Decls.(IsDefinition Definition)) in let inst, univs = match univs with | Polymorphic_entry (_, uctx) -> Univ.UContext.instance uctx, univs @@ -513,7 +512,7 @@ let declare_class def cum ubinders univs id idbuild paramimpls params arity it_mkLambda_or_LetIn (mkLambda (binder, inst_type, mkRel 1)) params in let proj_entry = Declare.definition_entry ~types:proj_type ~univs proj_body in let proj_cst = Declare.declare_constant proj_name - (DefinitionEntry proj_entry, IsDefinition Definition) + (DefinitionEntry proj_entry, Decls.(IsDefinition Definition)) in let cref = ConstRef cst in Impargs.declare_manual_implicits false cref paramimpls; @@ -528,7 +527,7 @@ let declare_class def cum ubinders univs id idbuild paramimpls params arity let record_data = [id, idbuild, arity, fieldimpls, fields, false, List.map (fun _ -> { pf_subclass = false ; pf_canonical = true }) fields] in let inds = declare_structure ~cum Declarations.BiFinite ubinders univs paramimpls - params template ~kind:Method ~name:[|binder_name|] record_data + params template ~kind:Decls.Method ~name:[|binder_name|] record_data in let coers = List.map2 (fun coe pri -> Option.map (fun b -> diff --git a/vernac/record.mli b/vernac/record.mli index d0164572f3..3165448d0c 100644 --- a/vernac/record.mli +++ b/vernac/record.mli @@ -22,7 +22,7 @@ type projection_flags = { val declare_projections : inductive -> Entries.universes_entry -> - ?kind:Decl_kinds.definition_object_kind -> + ?kind:Decls.definition_object_kind -> Id.t -> projection_flags list -> Impargs.manual_implicits list -> diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 9b9be0209e..cfa25b03bc 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -24,7 +24,6 @@ open Goptions open Libnames open Globnames open Vernacexpr -open Decl_kinds open Constrexpr open Redexpr open Lemmas @@ -525,7 +524,7 @@ let start_proof_and_print ~program_mode ~poly ?hook ~scope ~kind l = in start_lemma_com ~program_mode ?inference_hook ?hook ~poly ~scope ~kind l -let vernac_definition_hook ~poly = function +let vernac_definition_hook ~poly = let open Decls in function | Coercion -> Some (Class.add_coercion_hook ~poly) | CanonicalStructure -> @@ -558,7 +557,7 @@ let vernac_definition_interactive ~atts (discharge, kind) (lid, pl) bl t = let program_mode = atts.program in let poly = atts.polymorphic in let name = vernac_definition_name lid local in - start_proof_and_print ~program_mode ~poly ~scope:local ~kind:(DefinitionBody kind) ?hook [(name, pl), (bl, t)] + start_proof_and_print ~program_mode ~poly ~scope:local ~kind:(Decls.DefinitionBody kind) ?hook [(name, pl), (bl, t)] let vernac_definition ~atts (discharge, kind) (lid, pl) bl red_option c typ_opt = let open DefAttributes in @@ -581,7 +580,7 @@ let vernac_start_proof ~atts kind l = let scope = enforce_locality_exp atts.locality NoDischarge in if Dumpglob.dump () then List.iter (fun ((id, _), _) -> Dumpglob.dump_definition id false "prf") l; - start_proof_and_print ~program_mode:atts.program ~poly:atts.polymorphic ~scope ~kind:(Proof kind) l + start_proof_and_print ~program_mode:atts.program ~poly:atts.polymorphic ~scope ~kind:(Decls.Proof kind) l let vernac_end_proof ~lemma = let open Vernacexpr in function | Admitted -> diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml index dc5df5904e..eb1bca410a 100644 --- a/vernac/vernacexpr.ml +++ b/vernac/vernacexpr.ml @@ -276,11 +276,11 @@ type nonrec vernac_expr = | VernacDeclareCustomEntry of string (* Gallina *) - | VernacDefinition of (discharge * Decl_kinds.definition_object_kind) * name_decl * definition_expr - | VernacStartTheoremProof of Decl_kinds.theorem_kind * proof_expr list + | VernacDefinition of (discharge * Decls.definition_object_kind) * name_decl * definition_expr + | VernacStartTheoremProof of Decls.theorem_kind * proof_expr list | VernacEndProof of proof_end | VernacExactProof of constr_expr - | VernacAssumption of (discharge * Decl_kinds.assumption_object_kind) * + | VernacAssumption of (discharge * Decls.assumption_object_kind) * Declaremods.inline * (ident_decl list * constr_expr) with_coercion list | VernacInductive of vernac_cumulative option * Decl_kinds.private_flag * inductive_flag * (inductive_expr * decl_notation list) list | VernacFixpoint of discharge * (fixpoint_expr * decl_notation list) list |