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