From e5b3bd6b12af9f08d7913e25748fba9c4f9fd48f Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sat, 29 Sep 2018 18:20:36 +0200 Subject: [api] Cleanup `Decls`: remove unused function, move vernac helper. It seems these two functions don't belong there. We can remove one, and place the other actually next to whether their semantics are necessary. Note that indeed the whole `Decls` file seems a bit suspicious, why we do we register this information in a separate table instead of in the main ones in `Lib` ? At the suggestion of Gaëtan Gilbert we also remove unused function `is_instance`. --- library/decls.ml | 22 ---------------------- library/decls.mli | 9 --------- pretyping/typeclasses.ml | 14 -------------- pretyping/typeclasses.mli | 3 +-- vernac/lemmas.ml | 8 ++++++++ vernac/lemmas.mli | 6 +++++- vernac/obligations.ml | 4 ++-- 7 files changed, 16 insertions(+), 50 deletions(-) diff --git a/library/decls.ml b/library/decls.ml index 12c820fb7d..b766b6e2cb 100644 --- a/library/decls.ml +++ b/library/decls.ml @@ -11,13 +11,10 @@ (** This module registers tables for some non-logical informations associated declarations *) -open Util open Names open Decl_kinds open Libnames -module NamedDecl = Context.Named.Declaration - (** Datas associated to section variables and local definitions *) type variable_data = @@ -47,22 +44,3 @@ let csttab = Summary.ref (Cmap.empty : logical_kind Cmap.t) ~name:"CONSTANT" let add_constant_kind kn k = csttab := Cmap.add kn k !csttab let constant_kind kn = Cmap.find kn !csttab - -(** Miscellaneous functions. *) - -let initialize_named_context_for_proof () = - let sign = Global.named_context () in - List.fold_right - (fun d signv -> - let id = NamedDecl.get_id d in - let d = if variable_opacity id then NamedDecl.LocalAssum (id, NamedDecl.get_type d) else d in - Environ.push_named_context_val d signv) sign Environ.empty_named_context_val - -let last_section_hyps dir = - Context.Named.fold_outside - (fun d sec_ids -> - let id = NamedDecl.get_id d in - try if DirPath.equal dir (variable_path id) then id::sec_ids else sec_ids - with Not_found -> sec_ids) - (Environ.named_context (Global.env())) - ~init:[] diff --git a/library/decls.mli b/library/decls.mli index d9fc291518..401884736e 100644 --- a/library/decls.mli +++ b/library/decls.mli @@ -34,12 +34,3 @@ val variable_exists : variable -> bool val add_constant_kind : Constant.t -> logical_kind -> unit val constant_kind : Constant.t -> logical_kind - -(* Prepare global named context for proof session: remove proofs of - opaque section definitions and remove vm-compiled code *) - -val initialize_named_context_for_proof : unit -> Environ.named_context_val - -(** Miscellaneous functions *) - -val last_section_hyps : DirPath.t -> Id.t list diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index 55d9838bbb..67c5643459 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -11,7 +11,6 @@ (*i*) open Names open Globnames -open Decl_kinds open Term open Constr open Vars @@ -482,19 +481,6 @@ let instances r = let is_class gr = GlobRef.Map.exists (fun _ v -> GlobRef.equal v.cl_impl gr) !classes -let is_instance = function - | ConstRef c -> - (match Decls.constant_kind c with - | IsDefinition Instance -> true - | _ -> false) - | VarRef v -> - (match Decls.variable_kind v with - | IsDefinition Instance -> true - | _ -> false) - | ConstructRef (ind,_) -> - is_class (IndRef ind) - | _ -> false - (* To embed a boolean for resolvability status. This is essentially a hack to mark which evars correspond to goals and do not need to be resolved when we have nested [resolve_all_evars] diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli index 80c6d82397..f0437be4ed 100644 --- a/pretyping/typeclasses.mli +++ b/pretyping/typeclasses.mli @@ -79,13 +79,12 @@ val typeclass_univ_instance : typeclass Univ.puniverses -> typeclass (** Just return None if not a class *) val class_of_constr : evar_map -> EConstr.constr -> (EConstr.rel_context * ((typeclass * EConstr.EInstance.t) * constr list)) option - + val instance_impl : instance -> GlobRef.t val hint_priority : instance -> int option val is_class : GlobRef.t -> bool -val is_instance : GlobRef.t -> bool (** Returns the term and type for the given instance of the parameters and fields of the type class. *) diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index 880a11becd..aa9bd20bf3 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -344,6 +344,14 @@ let universe_proof_terminator compute_guard hook = let standard_proof_terminator compute_guard hook = universe_proof_terminator compute_guard (fun _ -> hook) +let initialize_named_context_for_proof () = + let sign = Global.named_context () in + List.fold_right + (fun d signv -> + let id = NamedDecl.get_id d in + let d = if variable_opacity id then NamedDecl.LocalAssum (id, NamedDecl.get_type d) else d in + Environ.push_named_context_val d signv) sign Environ.empty_named_context_val + let start_proof id ?pl kind sigma ?terminator ?sign c ?init_tac ?(compute_guard=[]) hook = let terminator = match terminator with | None -> standard_proof_terminator compute_guard hook diff --git a/vernac/lemmas.mli b/vernac/lemmas.mli index c9e4876ee3..38683ed6b2 100644 --- a/vernac/lemmas.mli +++ b/vernac/lemmas.mli @@ -56,6 +56,11 @@ val standard_proof_terminator : val fresh_name_for_anonymous_theorem : unit -> Id.t +(* Prepare global named context for proof session: remove proofs of + opaque section definitions and remove vm-compiled code *) + +val initialize_named_context_for_proof : unit -> Environ.named_context_val + (** {6 ... } *) (** A hook the next three functions pass to cook_proof *) @@ -63,7 +68,6 @@ val set_save_hook : (Proof.t -> unit) -> unit val save_proof : ?proof:Proof_global.closed_proof -> Vernacexpr.proof_end -> unit - (** [get_current_context ()] returns the evar context and env of the current open proof if any, otherwise returns the empty evar context and the current global env *) diff --git a/vernac/obligations.ml b/vernac/obligations.ml index 3987e53bc7..c4a10b4be6 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -1102,7 +1102,7 @@ let show_term n = let add_definition n ?term t ctx ?(univdecl=UState.default_univ_decl) ?(implicits=[]) ?(kind=Global,false,Definition) ?tactic ?(reduce=reduce) ?(hook=Lemmas.mk_hook (fun _ _ _ -> ())) ?(opaque = false) obls = - let sign = Decls.initialize_named_context_for_proof () in + let sign = Lemmas.initialize_named_context_for_proof () in let info = Id.print n ++ str " has type-checked" in let prg = init_prog_info sign ~opaque n univdecl term t ctx [] None [] obls implicits kind reduce hook in let obls,_ = prg.prg_obligations in @@ -1122,7 +1122,7 @@ let add_definition n ?term t ctx ?(univdecl=UState.default_univ_decl) let add_mutual_definitions l ctx ?(univdecl=UState.default_univ_decl) ?tactic ?(kind=Global,false,Definition) ?(reduce=reduce) ?(hook=Lemmas.mk_hook (fun _ _ _ -> ())) ?(opaque = false) notations fixkind = - let sign = Decls.initialize_named_context_for_proof () in + let sign = Lemmas.initialize_named_context_for_proof () in let deps = List.map (fun (n, b, t, imps, obls) -> n) l in List.iter (fun (n, b, t, imps, obls) -> -- cgit v1.2.3