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/term_typing.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'kernel/term_typing.ml')

diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 83d1ce16c4..33a4b55e87 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -42,9 +42,9 @@ let local_constrain_type env j cst1 = function
       assert (eq_constr t tj.utj_val);
       t, union_constraints (union_constraints cst1 cst2) cst3
 
-let translate_local_def env (b,topt) =
-  let (j,cst) = infer env b in
-  let (typ,cst) = local_constrain_type env j cst topt in
+let translate_local_def env de =
+  let (j,cst) = infer env de.const_entry_body in
+  let (typ,cst) = local_constrain_type env j cst de.const_entry_type in
     (j.uj_val,typ,cst)
 
 let translate_local_assum env t =
-- 
cgit v1.2.3