diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-11-19 10:38:25 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-11-19 10:38:25 +0000 |
| commit | 79ac780518b797b9e2181ef3993cb08c202b130a (patch) | |
| tree | ab5ecd5546cc33b6aaa65afd4875c7560abfc64c /kernel | |
| parent | 458fdba7a34fdf49f4f93e6734e90c6603c61adf (diff) | |
Mise en place d'une méthode directe pour indiquer le type des déclarations à toplevel plutôt que de passer par mkCast
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2203 85f007b7-540e-0410-9357-904b9bb8a0f7
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 |