diff options
| author | Pierre-Marie Pédrot | 2018-10-03 14:48:43 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-10-03 14:48:43 +0200 |
| commit | 920cc6ba6ee33bf34cd853f6a9a050ed7594e2ce (patch) | |
| tree | c3874e606bdbac3bf6c3f093587e5dda8dae37ec /library | |
| parent | 016f4a302090bcbb4ad47197dda2c60d6f598f6a (diff) | |
| parent | e5b3bd6b12af9f08d7913e25748fba9c4f9fd48f (diff) | |
Merge PR #8596: [api] Cleanup `Decls`: remove unused function, move vernac helper.
Diffstat (limited to 'library')
| -rw-r--r-- | library/decls.ml | 22 | ||||
| -rw-r--r-- | library/decls.mli | 9 |
2 files changed, 0 insertions, 31 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 |