summaryrefslogtreecommitdiff
path: root/library/decls.mli
diff options
context:
space:
mode:
Diffstat (limited to 'library/decls.mli')
-rw-r--r--library/decls.mli12
1 files changed, 7 insertions, 5 deletions
diff --git a/library/decls.mli b/library/decls.mli
index 7a8e138b..73f1745b 100644
--- a/library/decls.mli
+++ b/library/decls.mli
@@ -1,13 +1,11 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: decls.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
open Names
open Sign
open Libnames
@@ -20,7 +18,7 @@ open Decl_kinds
(** Registration and access to the table of variable *)
type variable_data =
- dir_path * bool (* opacity *) * Univ.constraints * logical_kind
+ dir_path * bool (** opacity *) * Univ.constraints * logical_kind
val add_variable_data : variable -> variable_data -> unit
val variable_path : variable -> dir_path
@@ -35,7 +33,11 @@ val variable_exists : variable -> bool
val add_constant_kind : constant -> logical_kind -> unit
val constant_kind : constant -> 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 : dir_path -> identifier list
-val clear_proofs : named_context -> Environ.named_context_val