From 1eaebf4ab7616b2be16b957736e80f1d6100eae0 Mon Sep 17 00:00:00 2001
From: gareuselesinge
Date: Thu, 9 May 2013 20:48:29 +0000
Subject: Use definition_entry to declare local definitions

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16502 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/safe_typing.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'kernel/safe_typing.mli')

diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index 46dac02aa1..31bb8143e9 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -34,7 +34,7 @@ val push_named_assum :
   Id.t * types -> safe_environment ->
     Univ.constraints * safe_environment
 val push_named_def :
-  Id.t * constr * types option -> safe_environment ->
+  Id.t * definition_entry -> safe_environment ->
     Univ.constraints * safe_environment
 
 (** Adding global axioms or definitions *)
-- 
cgit v1.2.3