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/decls.mli | |
| parent | 016f4a302090bcbb4ad47197dda2c60d6f598f6a (diff) | |
| parent | e5b3bd6b12af9f08d7913e25748fba9c4f9fd48f (diff) | |
Merge PR #8596: [api] Cleanup `Decls`: remove unused function, move vernac helper.
Diffstat (limited to 'library/decls.mli')
| -rw-r--r-- | library/decls.mli | 9 |
1 files changed, 0 insertions, 9 deletions
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 |