diff options
| author | herbelin | 2001-11-19 10:38:25 +0000 |
|---|---|---|
| committer | herbelin | 2001-11-19 10:38:25 +0000 |
| commit | 79ac780518b797b9e2181ef3993cb08c202b130a (patch) | |
| tree | ab5ecd5546cc33b6aaa65afd4875c7560abfc64c /library | |
| 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 'library')
| -rw-r--r-- | library/declare.ml | 6 | ||||
| -rw-r--r-- | library/declare.mli | 4 | ||||
| -rw-r--r-- | library/global.mli | 2 |
3 files changed, 6 insertions, 6 deletions
diff --git a/library/declare.ml b/library/declare.ml index 816a456154..542bd6b946 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -66,8 +66,8 @@ let make_strength_2 () = (* Section variables. *) type section_variable_entry = - | SectionLocalDef of constr - | SectionLocalAssum of constr + | SectionLocalDef of constr * types option + | SectionLocalAssum of types type variable_declaration = dir_path * section_variable_entry * strength @@ -90,7 +90,7 @@ let cache_variable (sp,(id,(p,d,str))) = errorlabstrm "cache_variable" [< pr_id id; 'sTR " already exists" >]; let cst = match d with (* Fails if not well-typed *) | SectionLocalAssum ty -> Global.push_named_assum (id,ty) - | SectionLocalDef c -> Global.push_named_def (id,c) in + | SectionLocalDef (c,t) -> Global.push_named_def (id,c,t) in let (_,bd,ty) = Global.lookup_named id in let vd = (bd,ty,cst) in Nametab.push 0 (restrict_path 0 sp) (VarRef id); diff --git a/library/declare.mli b/library/declare.mli index c57dd2079c..bb903a9c46 100644 --- a/library/declare.mli +++ b/library/declare.mli @@ -32,8 +32,8 @@ type strength = | NeverDischarge type section_variable_entry = - | SectionLocalDef of constr - | SectionLocalAssum of constr + | SectionLocalDef of constr * types option + | SectionLocalAssum of types type variable_declaration = dir_path * section_variable_entry * strength diff --git a/library/global.mli b/library/global.mli index 6e352e2f8f..f10ab98a5a 100644 --- a/library/global.mli +++ b/library/global.mli @@ -29,7 +29,7 @@ val named_context : unit -> Sign.named_context (* Extending env with variables, constants and inductives *) val push_named_assum : (identifier * types) -> Univ.constraints -val push_named_def : (identifier * constr) -> Univ.constraints +val push_named_def : (identifier * constr * types option) -> Univ.constraints val pop_named_decls : identifier list -> unit val add_parameter : constant -> types -> unit |