diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/entries.mli | 3 | ||||
| -rw-r--r-- | kernel/safe_typing.ml | 4 | ||||
| -rw-r--r-- | kernel/safe_typing.mli | 2 | ||||
| -rw-r--r-- | kernel/term_typing.ml | 6 | ||||
| -rw-r--r-- | kernel/term_typing.mli | 2 |
5 files changed, 9 insertions, 8 deletions
diff --git a/kernel/entries.mli b/kernel/entries.mli index b2d65d3ed..392a2cd84 100644 --- a/kernel/entries.mli +++ b/kernel/entries.mli @@ -47,9 +47,10 @@ type mutual_inductive_entry = { mind_entry_inds : one_inductive_entry list } (** {6 Constants (Definition/Axiom) } *) +type const_entry_body = constr type definition_entry = { - const_entry_body : constr; + const_entry_body : const_entry_body; const_entry_secctx : Context.section_context option; const_entry_type : types option; const_entry_opaque : bool; diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 851803621..62e2d46a8 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''}) diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index 46dac02aa..31bb8143e 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 *) diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index 83d1ce16c..33a4b55e8 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 = diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli index cc6025dab..c9bff84fc 100644 --- a/kernel/term_typing.mli +++ b/kernel/term_typing.mli @@ -13,7 +13,7 @@ open Environ open Declarations open Entries -val translate_local_def : env -> constr * types option -> +val translate_local_def : env -> definition_entry -> constr * types * constraints val translate_local_assum : env -> types -> types * constraints |