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/safe_typing.mli | 9 +++++++++
 1 file changed, 9 insertions(+)

(limited to 'kernel/safe_typing.mli')

diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index 1b4d932b59..fe028c073f 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -126,3 +126,12 @@ val safe_infer : safe_environment -> constr -> judgment * Univ.constraints
 val typing : safe_environment -> constr -> judgment
 
 
+
+(*spiwack: safe retroknowledge functionalities *)
+
+open Retroknowledge
+
+val retroknowledge : (retroknowledge-> 'a) -> safe_environment -> 'a
+
+val register : safe_environment -> field -> Retroknowledge.entry -> constr
+                                         -> safe_environment
-- 
cgit v1.2.3