From a6d663c85d71b3cce007af23419e8030b8c5ac88 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Mon, 25 May 2020 14:57:44 +0200 Subject: [declare] [api] Removal of duplicated type aliases. --- doc/plugin_tutorial/tuto1/src/simple_declare.ml | 2 +- plugins/funind/functional_principles_proofs.ml | 2 +- plugins/funind/gen_principle.ml | 24 +++++++------- plugins/funind/recdef.ml | 12 ++++--- plugins/ltac/rewrite.ml | 4 +-- stm/stm.ml | 8 ++--- stm/vernac_classifier.ml | 2 +- vernac/classes.ml | 4 +-- vernac/comAssumption.ml | 23 +++++++------- vernac/comAssumption.mli | 4 +-- vernac/comCoercion.ml | 4 +-- vernac/comDefinition.mli | 4 +-- vernac/comFixpoint.mli | 8 ++--- vernac/comHints.ml | 2 +- vernac/comProgramFixpoint.mli | 4 +-- vernac/declare.ml | 42 +++++++++++-------------- vernac/declare.mli | 18 ++++------- vernac/g_proofs.mlg | 8 ++--- vernac/obligations.ml | 8 ++--- vernac/obligations.mli | 4 +-- vernac/vernacentries.ml | 9 +++--- vernac/vernacstate.mli | 2 +- 22 files changed, 94 insertions(+), 104 deletions(-) diff --git a/doc/plugin_tutorial/tuto1/src/simple_declare.ml b/doc/plugin_tutorial/tuto1/src/simple_declare.ml index 5431a21b53..73292e0120 100644 --- a/doc/plugin_tutorial/tuto1/src/simple_declare.ml +++ b/doc/plugin_tutorial/tuto1/src/simple_declare.ml @@ -1,6 +1,6 @@ let declare_definition ~poly name sigma body = let udecl = UState.default_univ_decl in - let scope = Declare.Global Declare.ImportDefaultBehavior in + let scope = Locality.Global Locality.ImportDefaultBehavior in let kind = Decls.(IsDefinition Definition) in let info = Declare.CInfo.make ~scope ~kind ~impargs:[] ~udecl ~opaque:false ~poly () in Declare.declare_definition ~name ~info ~types:None ~body sigma diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index c0d7c1e8e6..6ec12db952 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -860,7 +860,7 @@ let generate_equation_lemma evd fnames f fun_num nb_params nb_args rec_args_num in let lemma, _ = Declare.by (Proofview.V82.tactic prove_replacement) lemma in let () = - Declare.save_lemma_proved ~proof:lemma ~opaque:Declare.Transparent + Declare.save_lemma_proved ~proof:lemma ~opaque:Vernacexpr.Transparent ~idopt:None in evd diff --git a/plugins/funind/gen_principle.ml b/plugins/funind/gen_principle.ml index 30069c9914..8a07c2109e 100644 --- a/plugins/funind/gen_principle.ml +++ b/plugins/funind/gen_principle.ml @@ -319,7 +319,7 @@ let generate_functional_principle (evd : Evd.evar_map ref) old_princ_type sorts let entry = Declare.definition_entry ~univs ?types body in let (_ : Names.GlobRef.t) = Declare.declare_entry ~name:new_princ_name ~hook - ~scope:(Declare.Global Declare.ImportDefaultBehavior) + ~scope:(Locality.Global Locality.ImportDefaultBehavior) ~kind:Decls.(IsProof Theorem) ~impargs:[] ~uctx entry in @@ -400,7 +400,7 @@ let register_struct is_rec fixpoint_exprl = Pp.(str "Body of Function must be given") in ComDefinition.do_definition ~name:fname.CAst.v ~poly:false - ~scope:(Declare.Global Declare.ImportDefaultBehavior) + ~scope:(Locality.Global Locality.ImportDefaultBehavior) ~kind:Decls.Definition univs binders None body (Some rtype); let evd, rev_pconstants = List.fold_left @@ -419,7 +419,7 @@ let register_struct is_rec fixpoint_exprl = (None, evd, List.rev rev_pconstants) | _ -> ComFixpoint.do_fixpoint - ~scope:(Declare.Global Declare.ImportDefaultBehavior) ~poly:false + ~scope:(Locality.Global Locality.ImportDefaultBehavior) ~poly:false fixpoint_exprl; let evd, rev_pconstants = List.fold_left @@ -1370,12 +1370,12 @@ let make_scheme evd (fas : (Constr.pconstant * Sorts.family) list) : _ list = | None -> raise Not_found | Some finfos -> finfos in - let open Declare in match finfos.equation_lemma with - | None -> Transparent (* non recursive definition *) + | None -> Vernacexpr.Transparent (* non recursive definition *) | Some equation -> - if Declareops.is_opaque (Global.lookup_constant equation) then Opaque - else Transparent + if Declareops.is_opaque (Global.lookup_constant equation) then + Vernacexpr.Opaque + else Vernacexpr.Transparent in let body, typ, univs, _hook, sigma0 = try @@ -1527,8 +1527,8 @@ let derive_correctness (funs : Constr.pconstant list) (graphs : inductive list) fst @@ Declare.by (Proofview.V82.tactic (proving_tac i)) lemma in let () = - Declare.save_lemma_proved ~proof:lemma ~opaque:Declare.Transparent - ~idopt:None + Declare.save_lemma_proved ~proof:lemma + ~opaque:Vernacexpr.Transparent ~idopt:None in let finfo = match find_Function_infos (fst f_as_constant) with @@ -1600,8 +1600,8 @@ let derive_correctness (funs : Constr.pconstant list) (graphs : inductive list) lemma) in let () = - Declare.save_lemma_proved ~proof:lemma ~opaque:Declare.Transparent - ~idopt:None + Declare.save_lemma_proved ~proof:lemma + ~opaque:Vernacexpr.Transparent ~idopt:None in let finfo = match find_Function_infos (fst f_as_constant) with @@ -2205,7 +2205,7 @@ let build_scheme fas = List.iter2 (fun (princ_id, _, _) (body, types, univs, opaque) -> let (_ : Constant.t) = - let opaque = if opaque = Declare.Opaque then true else false in + let opaque = if opaque = Vernacexpr.Opaque then true else false in let def_entry = Declare.definition_entry ~univs ~opaque ?types body in Declare.declare_constant ~name:princ_id ~kind:Decls.(IsProof Theorem) diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 58ed3864bb..853a54592d 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -58,7 +58,8 @@ let declare_fun name kind ?univs value = (Declare.declare_constant ~name ~kind (Declare.DefinitionEntry ce)) let defined lemma = - Declare.save_lemma_proved ~proof:lemma ~opaque:Declare.Transparent ~idopt:None + Declare.save_lemma_proved ~proof:lemma ~opaque:Vernacexpr.Transparent + ~idopt:None let def_of_const t = match Constr.kind t with @@ -1414,11 +1415,12 @@ let build_new_goal_type lemma = let is_opaque_constant c = let cb = Global.lookup_constant c in + let open Vernacexpr in match cb.Declarations.const_body with - | Declarations.OpaqueDef _ -> Declare.Opaque - | Declarations.Undef _ -> Declare.Opaque - | Declarations.Def _ -> Declare.Transparent - | Declarations.Primitive _ -> Declare.Opaque + | Declarations.OpaqueDef _ -> Opaque + | Declarations.Undef _ -> Opaque + | Declarations.Def _ -> Transparent + | Declarations.Primitive _ -> Opaque let open_new_goal ~lemma build_proof sigma using_lemmas ref_ goal_name (gls_type, decompose_and_tac, nb_goal) = diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index 67d09acfda..0bf97fefa6 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -1900,7 +1900,7 @@ let declare_projection name instance_id r = in it_mkProd_or_LetIn ccl ctx in let types = Some (it_mkProd_or_LetIn typ ctx) in - let kind, opaque, scope = Decls.(IsDefinition Definition), false, Declare.Global Declare.ImportDefaultBehavior in + let kind, opaque, scope = Decls.(IsDefinition Definition), false, Locality.Global Locality.ImportDefaultBehavior in let impargs, udecl = [], UState.default_univ_decl in let info = Declare.CInfo.make ~scope ~kind ~opaque ~impargs ~udecl ~poly () in let _r : GlobRef.t = @@ -1968,7 +1968,7 @@ let add_morphism_as_parameter atts m n : unit = let env = Global.env () in let evd = Evd.from_env env in let poly = atts.polymorphic in - let kind, opaque, scope = Decls.(IsAssumption Logical), false, Declare.Global Declare.ImportDefaultBehavior in + let kind, opaque, scope = Decls.(IsAssumption Logical), false, Locality.Global Locality.ImportDefaultBehavior in let impargs, udecl = [], UState.default_univ_decl in let evd, types = build_morphism_signature env evd m in let evd, pe = Declare.prepare_parameter ~poly ~udecl ~types evd in diff --git a/stm/stm.ml b/stm/stm.ml index 7aaa359149..800115ce42 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -1523,7 +1523,7 @@ end = struct (* {{{ *) PG_compat.close_future_proof ~feedback_id:stop (Future.from_val proof) in let st = Vernacstate.freeze_interp_state ~marshallable:false in - let opaque = Declare.Opaque in + let opaque = Opaque in try let _pstate = stm_qed_delay_proof ~st ~id:stop @@ -1667,7 +1667,7 @@ end = struct (* {{{ *) let _proof = PG_compat.return_partial_proof () in `OK_ADMITTED else begin - let opaque = Declare.Opaque in + let opaque = Opaque in (* The original terminator, a hook, has not been saved in the .vio*) let proof, _info = @@ -2162,7 +2162,7 @@ let collect_proof keep cur hd brkind id = | id :: _ -> Names.Id.to_string id in let loc = (snd cur).expr.CAst.loc in let is_defined_expr = function - | VernacEndProof (Proved (Declare.Transparent,_)) -> true + | VernacEndProof (Proved (Transparent,_)) -> true | _ -> false in let is_defined = function | _, { expr = e } -> is_defined_expr e.CAst.v.expr @@ -2527,7 +2527,7 @@ let known_state ~doc ?(redefine_qed=false) ~cache id = | VtKeep VtKeepAxiom -> qed.fproof <- Some (None, ref false); None | VtKeep opaque -> - let opaque = let open Declare in match opaque with + let opaque = match opaque with | VtKeepOpaque -> Opaque | VtKeepDefined -> Transparent | VtKeepAxiom -> assert false in diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml index cf127648b4..a957f7354f 100644 --- a/stm/vernac_classifier.ml +++ b/stm/vernac_classifier.ml @@ -37,7 +37,7 @@ let string_of_vernac_classification = function | VtMeta -> "Meta " | VtProofMode _ -> "Proof Mode" -let vtkeep_of_opaque = let open Declare in function +let vtkeep_of_opaque = function | Opaque -> VtKeepOpaque | Transparent -> VtKeepDefined diff --git a/vernac/classes.ml b/vernac/classes.ml index c4c6a0fa33..b36a6fa3a6 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -313,7 +313,7 @@ let instance_hook info global ?hook cst = let declare_instance_constant iinfo global impargs ?hook name udecl poly sigma term termtype = let kind = Decls.(IsDefinition Instance) in - let scope = Declare.Global Declare.ImportDefaultBehavior in + let scope = Locality.Global Locality.ImportDefaultBehavior in let info = Declare.CInfo.make ~kind ~scope ~impargs ~opaque:false ~poly ~udecl () in let kn = Declare.declare_definition ~name ~info ~types:(Some termtype) ~body:term sigma in instance_hook iinfo global ?hook kn @@ -344,7 +344,7 @@ let declare_instance_program env sigma ~global ~poly name pri impargs udecl term let obls, _, term, typ = RetrieveObl.retrieve_obligations env name sigma 0 term termtype in let hook = Declare.Hook.make hook in let uctx = Evd.evar_universe_context sigma in - let scope, kind = Declare.Global Declare.ImportDefaultBehavior, + let scope, kind = Locality.Global Locality.ImportDefaultBehavior, Decls.IsDefinition Decls.Instance in let _ : Declare.progress = Obligations.add_definition ~name ~term ~udecl ~scope ~poly ~kind ~hook ~impargs ~uctx typ obls diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml index 9c82eb8960..d8475126ca 100644 --- a/vernac/comAssumption.ml +++ b/vernac/comAssumption.ml @@ -61,8 +61,8 @@ let declare_axiom is_coe ~poly ~local ~kind typ (univs, pl) imps nl {CAst.v=name let sigma = Evd.from_env env in let () = if do_instance then Classes.declare_instance env sigma None false gr in let local = match local with - | Declare.ImportNeedQualified -> true - | Declare.ImportDefaultBehavior -> false + | Locality.ImportNeedQualified -> true + | Locality.ImportDefaultBehavior -> false in let () = if is_coe then ComCoercion.try_add_new_coercion gr ~local ~poly in let inst = instance_of_univ_entry univs in @@ -86,11 +86,11 @@ let context_set_of_entry = function | Monomorphic_entry uctx -> uctx let declare_assumptions ~poly ~scope ~kind univs nl l = - let () = let open Declare in match scope with - | Discharge -> + let () = match scope with + | Locality.Discharge -> (* declare universes separately for variables *) DeclareUctx.declare_universe_context ~poly (context_set_of_entry (fst univs)) - | Global _ -> () + | Locality.Global _ -> () in let _, _ = List.fold_left (fun (subst,univs) ((is_coe,idl),typ,imps) -> (* NB: here univs are ignored when scope=Discharge *) @@ -98,10 +98,10 @@ let declare_assumptions ~poly ~scope ~kind univs nl l = let univs,subst' = List.fold_left_map (fun univs id -> let refu = match scope with - | Declare.Discharge -> + | Locality.Discharge -> declare_variable is_coe ~kind typ imps Glob_term.Explicit id; GlobRef.VarRef id.CAst.v, Univ.Instance.empty - | Declare.Global local -> + | Locality.Global local -> declare_axiom is_coe ~local ~poly ~kind typ univs imps nl id in next_univs univs, (id.CAst.v, Constr.mkRef refu)) @@ -128,9 +128,8 @@ let process_assumptions_udecls ~scope l = udecl, id | (_, ([], _))::_ | [] -> assert false in - let open Declare in let () = match scope, udecl with - | Discharge, Some _ -> + | Locality.Discharge, Some _ -> let loc = first_id.CAst.loc in let msg = Pp.str "Section variables cannot be polymorphic." in user_err ?loc msg @@ -206,7 +205,7 @@ let context_insection sigma ~poly ctx = let uctx = Evd.evar_universe_context sigma in let kind = Decls.(IsDefinition Definition) in let _ : GlobRef.t = - Declare.declare_entry ~name ~scope:Declare.Discharge + Declare.declare_entry ~name ~scope:Locality.Discharge ~kind ~impargs:[] ~uctx entry in () @@ -237,8 +236,8 @@ let context_nosection sigma ~poly ctx = let entry = Declare.definition_entry ~univs ~types:t b in Declare.DefinitionEntry entry in - let local = if Lib.is_modtype () then Declare.ImportDefaultBehavior - else Declare.ImportNeedQualified + let local = if Lib.is_modtype () then Locality.ImportDefaultBehavior + else Locality.ImportNeedQualified in let cst = Declare.declare_constant ~name ~kind ~local decl in let () = Declare.assumption_message name in diff --git a/vernac/comAssumption.mli b/vernac/comAssumption.mli index 989015a9f3..3d425ad768 100644 --- a/vernac/comAssumption.mli +++ b/vernac/comAssumption.mli @@ -17,7 +17,7 @@ open Constrexpr val do_assumptions : program_mode:bool -> poly:bool - -> scope:Declare.locality + -> scope:Locality.locality -> kind:Decls.assumption_object_kind -> Declaremods.inline -> (ident_decl list * constr_expr) with_coercion list @@ -35,7 +35,7 @@ val declare_variable val declare_axiom : coercion_flag -> poly:bool - -> local:Declare.import_status + -> local:Locality.import_status -> kind:Decls.assumption_object_kind -> Constr.types -> Entries.universes_entry * UnivNames.universe_binders diff --git a/vernac/comCoercion.ml b/vernac/comCoercion.ml index 3cc5dd65af..15d8ebc4b5 100644 --- a/vernac/comCoercion.ml +++ b/vernac/comCoercion.ml @@ -354,7 +354,7 @@ let try_add_new_coercion_with_source ref ~local ~poly ~source = try_add_new_coercion_core ref ~local poly (Some source) None false let add_coercion_hook poly { Declare.Hook.S.scope; dref; _ } = - let open Declare in + let open Locality in let local = match scope with | Discharge -> assert false (* Local Coercion in section behaves like Local Definition *) | Global ImportNeedQualified -> true @@ -367,7 +367,7 @@ let add_coercion_hook poly { Declare.Hook.S.scope; dref; _ } = let add_coercion_hook ~poly = Declare.Hook.make (add_coercion_hook poly) let add_subclass_hook ~poly { Declare.Hook.S.scope; dref; _ } = - let open Declare in + let open Locality in let stre = match scope with | Discharge -> assert false (* Local Subclass in section behaves like Local Definition *) | Global ImportNeedQualified -> true diff --git a/vernac/comDefinition.mli b/vernac/comDefinition.mli index 2b846f17e0..e3417d0062 100644 --- a/vernac/comDefinition.mli +++ b/vernac/comDefinition.mli @@ -17,7 +17,7 @@ open Constrexpr val do_definition : ?hook:Declare.Hook.t -> name:Id.t - -> scope:Declare.locality + -> scope:Locality.locality -> poly:bool -> kind:Decls.definition_object_kind -> universe_decl_expr option @@ -30,7 +30,7 @@ val do_definition val do_definition_program : ?hook:Declare.Hook.t -> name:Id.t - -> scope:Declare.locality + -> scope:Locality.locality -> poly:bool -> kind:Decls.logical_kind -> universe_decl_expr option diff --git a/vernac/comFixpoint.mli b/vernac/comFixpoint.mli index 486d0156f9..aa5446205c 100644 --- a/vernac/comFixpoint.mli +++ b/vernac/comFixpoint.mli @@ -16,16 +16,16 @@ open Vernacexpr (** Entry points for the vernacular commands Fixpoint and CoFixpoint *) val do_fixpoint_interactive : - scope:Declare.locality -> poly:bool -> fixpoint_expr list -> Declare.Proof.t + scope:Locality.locality -> poly:bool -> fixpoint_expr list -> Declare.Proof.t val do_fixpoint : - scope:Declare.locality -> poly:bool -> fixpoint_expr list -> unit + scope:Locality.locality -> poly:bool -> fixpoint_expr list -> unit val do_cofixpoint_interactive : - scope:Declare.locality -> poly:bool -> cofixpoint_expr list -> Declare.Proof.t + scope:Locality.locality -> poly:bool -> cofixpoint_expr list -> Declare.Proof.t val do_cofixpoint : - scope:Declare.locality -> poly:bool -> cofixpoint_expr list -> unit + scope:Locality.locality -> poly:bool -> cofixpoint_expr list -> unit (************************************************************************) (** Internal API *) diff --git a/vernac/comHints.ml b/vernac/comHints.ml index ec37ec7fa8..b05bf9a675 100644 --- a/vernac/comHints.ml +++ b/vernac/comHints.ml @@ -56,7 +56,7 @@ let project_hint ~poly pri l2r r = Declare.(DefinitionEntry (definition_entry ~univs:ctx ~opaque:false c)) in let c = - Declare.declare_constant ~local:Declare.ImportDefaultBehavior ~name + Declare.declare_constant ~local:Locality.ImportDefaultBehavior ~name ~kind:Decls.(IsDefinition Definition) cb in diff --git a/vernac/comProgramFixpoint.mli b/vernac/comProgramFixpoint.mli index 8b1fa6c202..e39f62c348 100644 --- a/vernac/comProgramFixpoint.mli +++ b/vernac/comProgramFixpoint.mli @@ -14,8 +14,8 @@ open Vernacexpr val do_fixpoint : (* When [false], assume guarded. *) - scope:Declare.locality -> poly:bool -> fixpoint_expr list -> unit + scope:Locality.locality -> poly:bool -> fixpoint_expr list -> unit val do_cofixpoint : (* When [false], assume guarded. *) - scope:Declare.locality -> poly:bool -> cofixpoint_expr list -> unit + scope:Locality.locality -> poly:bool -> cofixpoint_expr list -> unit diff --git a/vernac/declare.ml b/vernac/declare.ml index fde332cb66..430639b637 100644 --- a/vernac/declare.ml +++ b/vernac/declare.ml @@ -16,8 +16,6 @@ open Names open Safe_typing module NamedDecl = Context.Named.Declaration -type opacity_flag = Vernacexpr.opacity_flag = Opaque | Transparent - (* Hooks naturally belong here as they apply to both definitions and lemmas *) module Hook = struct module S = struct @@ -284,8 +282,6 @@ let get_open_goals ps = (List.map (fun (l1,l2) -> List.length l1 + List.length l2) stack) + List.length shelf -type import_status = Locality.import_status = ImportDefaultBehavior | ImportNeedQualified - (** Declaration of constants and parameters *) type 'a proof_entry = { @@ -409,7 +405,9 @@ let close_proof ~opaque ~keep_body_ucst_separate ps = let { Proof.name; poly } = Proof.data proof in let unsafe_typ = keep_body_ucst_separate && not poly in let elist, uctx = prepare_proof ~unsafe_typ ps in - let opaque = match opaque with Opaque -> true | Transparent -> false in + let opaque = match opaque with + | Vernacexpr.Opaque -> true + | Vernacexpr.Transparent -> false in let make_entry ((((_ub, body) as b), eff), ((_ut, typ) as t)) = let utyp, ubody = @@ -435,7 +433,7 @@ type 'a constant_entry = type constant_obj = { cst_kind : Decls.logical_kind; - cst_locl : import_status; + cst_locl : Locality.import_status; } let load_constant i ((sp,kn), obj) = @@ -449,8 +447,8 @@ let load_constant i ((sp,kn), obj) = let open_constant f i ((sp,kn), obj) = (* Never open a local definition *) match obj.cst_locl with - | ImportNeedQualified -> () - | ImportDefaultBehavior -> + | Locality.ImportNeedQualified -> () + | Locality.ImportDefaultBehavior -> let con = Global.constant_of_delta_kn kn in if Libobject.in_filter_ref (GlobRef.ConstRef con) f then Nametab.push (Nametab.Exactly i) sp (GlobRef.ConstRef con) @@ -504,7 +502,7 @@ let register_constant kn kind local = update_tables kn let register_side_effect (c, role) = - let () = register_constant c Decls.(IsProof Theorem) ImportDefaultBehavior in + let () = register_constant c Decls.(IsProof Theorem) Locality.ImportDefaultBehavior in match role with | None -> () | Some (Evd.Schema (ind, kind)) -> DeclareScheme.declare_scheme kind [|ind,c|] @@ -661,14 +659,14 @@ let define_constant ~name cd = if unsafe || is_unsafe_typing_flags() then feedback_axiom(); kn -let declare_constant ?(local = ImportDefaultBehavior) ~name ~kind cd = +let declare_constant ?(local = Locality.ImportDefaultBehavior) ~name ~kind cd = let () = check_exists name in let kn = define_constant ~name cd in (* Register the libobjects attached to the constants *) let () = register_constant kn kind local in kn -let declare_private_constant ?role ?(local = ImportDefaultBehavior) ~name ~kind de = +let declare_private_constant ?role ?(local = Locality.ImportDefaultBehavior) ~name ~kind de = let kn, eff = let de = if not de.proof_entry_opaque then @@ -921,7 +919,7 @@ let next = let n = ref 0 in fun () -> incr n; !n let by tac = map_fold_proof (Proof.solve (Goal_select.SelectNth 1) None tac) -let build_constant_by_tactic ~name ?(opaque=Transparent) ~uctx ~sign ~poly typ tac = +let build_constant_by_tactic ~name ?(opaque=Vernacexpr.Transparent) ~uctx ~sign ~poly typ tac = let evd = Evd.from_ctx uctx in let info = Info.make () in let pf = start_proof_core ~name ~poly ~sign ~udecl:UState.default_univ_decl ~impargs:[] ~info evd typ in @@ -962,7 +960,7 @@ let declare_abstract ~name ~poly ~kind ~sign ~secsign ~opaque ~solve_tac sigma c let concl = EConstr.of_constr concl in let uctx = Evd.evar_universe_context sigma in let (const, safe, uctx) = - try build_constant_by_tactic ~name ~opaque:Transparent ~poly ~uctx ~sign:secsign concl solve_tac + try build_constant_by_tactic ~name ~opaque:Vernacexpr.Transparent ~poly ~uctx ~sign:secsign concl solve_tac with Logic_monad.TacticFailure e as src -> (* if the tactic [tac] fails, it reports a [TacticFailure e], which is an error irrelevant to the proof system (in fact it @@ -986,7 +984,7 @@ let declare_abstract ~name ~poly ~kind ~sign ~secsign ~opaque ~solve_tac sigma c (* do not compute the implicit arguments, it may be costly *) let () = Impargs.make_implicit_args false in (* ppedrot: seems legit to have abstracted subproofs as local*) - declare_private_constant ~local:ImportNeedQualified ~name ~kind const + declare_private_constant ~local:Locality.ImportNeedQualified ~name ~kind const in let cst, eff = Impargs.with_implicit_protection cst () in let inst = match const.proof_entry_universes with @@ -1033,8 +1031,6 @@ let declare_definition_scheme ~internal ~univs ~role ~name c = let _ = Ind_tables.declare_definition_scheme := declare_definition_scheme let _ = Abstract.declare_abstract := declare_abstract -type locality = Locality.locality = | Discharge | Global of import_status - module CInfo = struct type t = @@ -1043,13 +1039,13 @@ module CInfo = struct ; inline : bool ; kind : Decls.logical_kind ; udecl : UState.universe_decl - ; scope : locality + ; scope : Locality.locality ; impargs : Impargs.manual_implicits ; hook : Hook.t option } let make ?(poly=false) ?(opaque=false) ?(inline=false) ?(kind=Decls.(IsDefinition Definition)) - ?(udecl=UState.default_univ_decl) ?(scope=Global ImportNeedQualified) ?(impargs=[]) + ?(udecl=UState.default_univ_decl) ?(scope=Locality.Global Locality.ImportNeedQualified) ?(impargs=[]) ?hook () = { poly; opaque; inline; kind; udecl; scope; impargs; hook } @@ -1064,11 +1060,11 @@ let declare_entry_core ~name ~scope ~kind ?hook ~obls ~impargs ~uctx entry = in let ubind = UState.universe_binders uctx in let dref = match scope with - | Discharge -> + | Locality.Discharge -> let () = declare_variable_core ~name ~kind (SectionLocalDef entry) in if should_suggest then Proof_using.suggest_variable (Global.env ()) name; Names.GlobRef.VarRef name - | Global local -> + | Locality.Global local -> let kn = declare_constant ~name ~local ~kind (DefinitionEntry entry) in let gr = Names.GlobRef.ConstRef kn in if should_suggest then Proof_using.suggest_constant (Global.env ()) kn; @@ -1131,8 +1127,8 @@ let warn_let_as_axiom = let declare_assumption ~name ~scope ~hook ~impargs ~uctx pe = let local = match scope with - | Discharge -> warn_let_as_axiom name; ImportNeedQualified - | Global local -> local + | Locality.Discharge -> warn_let_as_axiom name; Locality.ImportNeedQualified + | Locality.Global local -> local in let kind = Decls.(IsAssumption Conjectural) in let decl = ParameterEntry pe in @@ -1390,7 +1386,7 @@ let declare_obligation prg obl ~uctx ~types ~body = (* ppedrot: seems legit to have obligations as local *) let constant = declare_constant ~name:obl.obl_name - ~local:ImportNeedQualified + ~local:Locality.ImportNeedQualified ~kind:Decls.(IsProof Property) (DefinitionEntry ce) in diff --git a/vernac/declare.mli b/vernac/declare.mli index 002328b63f..67389d2966 100644 --- a/vernac/declare.mli +++ b/vernac/declare.mli @@ -162,8 +162,6 @@ module Proof : sig val info : t -> Info.t end -type opacity_flag = Vernacexpr.opacity_flag = Opaque | Transparent - (** [start_proof ~name ~udecl ~poly sigma goals] starts a proof of name [name] with goals [goals] (a list of pairs of environment and conclusion); [poly] determines if the proof is universe @@ -219,7 +217,7 @@ type proof_object (** Used by the STM only to store info, should go away *) val get_po_name : proof_object -> Id.t -val close_proof : opaque:opacity_flag -> keep_body_ucst_separate:bool -> Proof.t -> proof_object +val close_proof : opaque:Vernacexpr.opacity_flag -> keep_body_ucst_separate:bool -> Proof.t -> proof_object (** Declaration of local constructions (Variable/Hypothesis/Local) *) @@ -252,8 +250,6 @@ val definition_entry -> constr -> Evd.side_effects proof_entry -type import_status = Locality.import_status = ImportDefaultBehavior | ImportNeedQualified - (** [declare_constant id cd] declares a global declaration (constant/parameter) with name [id] in the current section; it returns the full path of the declaration @@ -265,7 +261,7 @@ type import_status = Locality.import_status = ImportDefaultBehavior | ImportNeed for removal from the public API, use higher-level declare APIs instead *) val declare_constant - : ?local:import_status + : ?local:Locality.import_status -> name:Id.t -> kind:Decls.logical_kind -> Evd.side_effects constant_entry @@ -337,8 +333,6 @@ val get_current_goal_context : Proof.t -> Evd.evar_map * Environ.env environment and empty evar_map. *) val get_current_context : Proof.t -> Evd.evar_map * Environ.env -type locality = Locality.locality = Discharge | Global of import_status - (** Information for a constant *) module CInfo : sig @@ -351,7 +345,7 @@ module CInfo : sig -> ?kind : Decls.logical_kind (** Theorem, etc... *) -> ?udecl : UState.universe_decl - -> ?scope : locality + -> ?scope : Locality.locality (** locality *) -> ?impargs : Impargs.manual_implicits -> ?hook : Hook.t @@ -366,7 +360,7 @@ end instead *) val declare_entry : name:Id.t - -> scope:locality + -> scope:Locality.locality -> kind:Decls.logical_kind -> ?hook:Hook.t -> impargs:Impargs.manual_implicits @@ -390,7 +384,7 @@ val declare_definition val declare_assumption : name:Id.t - -> scope:locality + -> scope:Locality.locality -> hook:Hook.t option -> impargs:Impargs.manual_implicits -> uctx:UState.t @@ -532,7 +526,7 @@ end val save_lemma_proved : proof:Proof.t - -> opaque:opacity_flag + -> opaque:Vernacexpr.opacity_flag -> idopt:Names.lident option -> unit diff --git a/vernac/g_proofs.mlg b/vernac/g_proofs.mlg index 80a4de472c..ebec720ce2 100644 --- a/vernac/g_proofs.mlg +++ b/vernac/g_proofs.mlg @@ -64,12 +64,12 @@ GRAMMAR EXTEND Gram | IDENT "Existential"; n = natural; c = constr_body -> { VernacSolveExistential (n,c) } | IDENT "Admitted" -> { VernacEndProof Admitted } - | IDENT "Qed" -> { VernacEndProof (Proved (Declare.Opaque,None)) } + | IDENT "Qed" -> { VernacEndProof (Proved (Opaque,None)) } | IDENT "Save"; id = identref -> - { VernacEndProof (Proved (Declare.Opaque, Some id)) } - | IDENT "Defined" -> { VernacEndProof (Proved (Declare.Transparent,None)) } + { VernacEndProof (Proved (Opaque, Some id)) } + | IDENT "Defined" -> { VernacEndProof (Proved (Transparent,None)) } | IDENT "Defined"; id=identref -> - { VernacEndProof (Proved (Declare.Transparent,Some id)) } + { VernacEndProof (Proved (Transparent,Some id)) } | IDENT "Restart" -> { VernacRestart } | IDENT "Undo" -> { VernacUndo 1 } | IDENT "Undo"; n = natural -> { VernacUndo n } diff --git a/vernac/obligations.ml b/vernac/obligations.ml index 9209b95e34..c0105224bf 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -135,7 +135,7 @@ let rec solve_obligation prg num tac = then Error.depends user_num remaining in let obl = subst_deps_obl obls obl in - let scope = Declare.(Global Declare.ImportNeedQualified) in + let scope = Locality.Global Locality.ImportNeedQualified in let kind = kind_of_obligation (snd obl.obl_status) in let evd = Evd.from_ctx (Internal.get_uctx prg) in let evd = Evd.update_sigma_env evd (Global.env ()) in @@ -303,7 +303,7 @@ let msg_generating_obl name obls = let add_definition ~name ?term t ~uctx ?(udecl = UState.default_univ_decl) ?(impargs = []) ~poly - ?(scope = Declare.Global Declare.ImportDefaultBehavior) + ?(scope = Locality.Global Locality.ImportDefaultBehavior) ?(kind = Decls.(IsDefinition Definition)) ?tactic ?(reduce = reduce) ?hook ?(opaque = false) obls = let prg = @@ -326,7 +326,7 @@ let add_definition ~name ?term t ~uctx ?(udecl = UState.default_univ_decl) | _ -> res let add_mutual_definitions l ~uctx ?(udecl = UState.default_univ_decl) - ?tactic ~poly ?(scope = Declare.Global Declare.ImportDefaultBehavior) + ?tactic ~poly ?(scope = Locality.Global Locality.ImportDefaultBehavior) ?(kind = Decls.(IsDefinition Definition)) ?(reduce = reduce) ?hook ?(opaque = false) notations fixkind = let deps = List.map (fun ({Declare.Recthm.name; _}, _, _) -> name) l in @@ -367,7 +367,7 @@ let admit_prog prg = let x = subst_deps_obl obls x in let uctx = Internal.get_uctx prg in let univs = UState.univ_entry ~poly:false uctx in - let kn = Declare.declare_constant ~name:x.obl_name ~local:Declare.ImportNeedQualified + let kn = Declare.declare_constant ~name:x.obl_name ~local:Locality.ImportNeedQualified (Declare.ParameterEntry (None, (x.obl_type, univs), None)) ~kind:Decls.(IsAssumption Conjectural) in Declare.assumption_message x.obl_name; diff --git a/vernac/obligations.mli b/vernac/obligations.mli index 334f6d40bb..a3e0d3b5c1 100644 --- a/vernac/obligations.mli +++ b/vernac/obligations.mli @@ -73,7 +73,7 @@ val add_definition : -> ?udecl:UState.universe_decl (** Universe binders and constraints *) -> ?impargs:Impargs.manual_implicits -> poly:bool - -> ?scope:Declare.locality + -> ?scope:Locality.locality -> ?kind:Decls.logical_kind -> ?tactic:unit Proofview.tactic -> ?reduce:(constr -> constr) @@ -92,7 +92,7 @@ val add_mutual_definitions : -> ?udecl:UState.universe_decl (** Universe binders and constraints *) -> ?tactic:unit Proofview.tactic -> poly:bool - -> ?scope:Declare.locality + -> ?scope:Locality.locality -> ?kind:Decls.logical_kind -> ?reduce:(constr -> constr) -> ?hook:Declare.Hook.t diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index f7da2000e3..6295587844 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -466,7 +466,7 @@ let vernac_custom_entry ~module_local s = let check_name_freshness locality {CAst.loc;v=id} : unit = (* We check existence here: it's a bit late at Qed time *) if Nametab.exists_cci (Lib.make_path id) || Termops.is_section_variable id || - locality <> Declare.Discharge && Nametab.exists_cci (Lib.make_path_except_section id) + locality <> Locality.Discharge && Nametab.exists_cci (Lib.make_path_except_section id) then user_err ?loc (Id.print id ++ str " already exists.") @@ -548,7 +548,6 @@ let vernac_definition_name lid local = CAst.make ?loc (fresh_name_for_anonymous_theorem ()) | { v = Name.Name n; loc } -> CAst.make ?loc n in let () = - let open Declare in match local with | Discharge -> Dumpglob.dump_definition lid true "var" | Global _ -> Dumpglob.dump_definition lid false "def" @@ -604,7 +603,7 @@ let vernac_exact_proof ~lemma c = (* spiwack: for simplicity I do not enforce that "Proof proof_term" is called only at the beginning of a proof. *) let lemma, status = Declare.by (Tactics.exact_proof c) lemma in - let () = Declare.save_lemma_proved ~proof:lemma ~opaque:Declare.Opaque ~idopt:None in + let () = Declare.save_lemma_proved ~proof:lemma ~opaque:Opaque ~idopt:None in if not status then Feedback.feedback Feedback.AddedAxiom let vernac_assumption ~atts discharge kind l nl = @@ -614,8 +613,8 @@ let vernac_assumption ~atts discharge kind l nl = if Dumpglob.dump () then List.iter (fun (lid, _) -> match scope with - | Declare.Global _ -> Dumpglob.dump_definition lid false "ax" - | Declare.Discharge -> Dumpglob.dump_definition lid true "var") idl) l; + | Global _ -> Dumpglob.dump_definition lid false "ax" + | Discharge -> Dumpglob.dump_definition lid true "var") idl) l; ComAssumption.do_assumptions ~poly:atts.polymorphic ~program_mode:atts.program ~scope ~kind nl l let is_polymorphic_inductive_cumulativity = diff --git a/vernac/vernacstate.mli b/vernac/vernacstate.mli index 07c27dd849..62afdb92ff 100644 --- a/vernac/vernacstate.mli +++ b/vernac/vernacstate.mli @@ -74,7 +74,7 @@ module Declare : sig feedback_id:Stateid.t -> Declare.closed_proof_output Future.computation -> closed_proof - val close_proof : opaque:Declare.opacity_flag -> keep_body_ucst_separate:bool -> closed_proof + val close_proof : opaque:Vernacexpr.opacity_flag -> keep_body_ucst_separate:bool -> closed_proof val discard_all : unit -> unit val update_global_env : unit -> unit -- cgit v1.2.3