diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/safe_typing.ml | 9 | ||||
| -rw-r--r-- | kernel/safe_typing.mli | 2 |
2 files changed, 8 insertions, 3 deletions
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index c770e0237..fdb7c0d0c 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -38,10 +38,15 @@ let empty_environment = empty_env (* Insertion of variables (named and de Bruijn'ed). They are now typed before being added to the environment. *) -let push_rel_or_named_def push (id,b) env = +let push_rel_or_named_def push (id,b,topt) env = let (j,cst) = safe_infer env b in + let (t,cst) = match topt with + | None -> j.uj_type, cst + | Some t -> + let (jt,cstt) = safe_infer_type env t in + jt.utj_val, Constraint.union cst cstt in let env' = add_constraints cst env in - let env'' = push (id,Some j.uj_val,j.uj_type) env' in + let env'' = push (id,Some j.uj_val,t) env' in (cst,env'') let push_named_def = push_rel_or_named_def push_named_decl diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index 5f6697b4e..36c2bbb23 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -30,7 +30,7 @@ val push_named_assum : identifier * types -> safe_environment -> Univ.constraints * safe_environment val push_named_def : - identifier * constr -> safe_environment -> + identifier * constr * types option -> safe_environment -> Univ.constraints * safe_environment val pop_named_decls : identifier list -> safe_environment -> safe_environment |