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.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'kernel/safe_typing.ml')

diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 8518036213..62e2d46a85 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -245,8 +245,8 @@ let safe_push_named (id,_,_ as d) env =
     with Not_found -> () in
   Environ.push_named d env
 
-let push_named_def (id,b,topt) senv =
-  let (c,typ,cst) = Term_typing.translate_local_def senv.env (b,topt) in
+let push_named_def (id,de) senv =
+  let (c,typ,cst) = Term_typing.translate_local_def senv.env de in
   let senv' = add_constraints cst senv in
   let env'' = safe_push_named (id,Some c,typ) senv'.env in
   (cst, {senv' with env=env''})
-- 
cgit v1.2.3