diff options
| author | gareuselesinge | 2013-05-09 20:48:29 +0000 |
|---|---|---|
| committer | gareuselesinge | 2013-05-09 20:48:29 +0000 |
| commit | 1eaebf4ab7616b2be16b957736e80f1d6100eae0 (patch) | |
| tree | 947ba448881d084f271365a29a15b10e649d0767 /kernel/term_typing.ml | |
| parent | 6105951610e140828d5be2c187c927d2119c8df0 (diff) | |
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
Diffstat (limited to 'kernel/term_typing.ml')
| -rw-r--r-- | kernel/term_typing.ml | 6 |
1 files changed, 3 insertions, 3 deletions
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 = |