diff options
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 = |