From 2dbe106c09b60690b87e31e58d505b1f4e05b57f Mon Sep 17 00:00:00 2001
From: aspiwack
Date: Fri, 11 May 2007 17:00:58 +0000
Subject: Processor integers + Print assumption (see coqdev mailing list for
 the details).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9821 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/environ.mli | 24 ++++++++++++++++++++++++
 1 file changed, 24 insertions(+)

(limited to 'kernel/environ.mli')

diff --git a/kernel/environ.mli b/kernel/environ.mli
index 96c2ba2761..293c55a691 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -219,3 +219,27 @@ val insert_after_hyp : named_context_val -> variable ->
 
 val remove_hyps : identifier list -> (named_declaration -> named_declaration) -> (Pre_env.lazy_val -> Pre_env.lazy_val) -> named_context_val -> named_context_val * identifier list
 
+
+(* spiwack: functions manipulating the retroknowledge *)
+open Retroknowledge
+
+val retroknowledge : (retroknowledge->'a) -> env -> 'a
+
+val registered : env -> field -> bool
+
+val unregister : env -> field -> env
+
+val register : env -> field -> Retroknowledge.entry -> env
+
+(* spiwack: a few declarations for the "Print Assumption" command *)
+type assumption =
+  | Variable of identifier*Term.constr
+  | Axiom of constant*Term.constr
+
+module OrderedAssumption :  Set.OrderedType with type t = assumption
+
+module AssumptionSet : Set.S with type elt = assumption
+
+val needed_assumptions : constr -> env -> AssumptionSet.t
+
+
-- 
cgit v1.2.3