diff options
Diffstat (limited to 'library')
| -rw-r--r-- | library/declare.ml | 4 | ||||
| -rw-r--r-- | library/declare.mli | 2 |
2 files changed, 3 insertions, 3 deletions
diff --git a/library/declare.ml b/library/declare.ml index 7a15b48637..49d684ed67 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -41,7 +41,7 @@ let make_strength_2 () = type section_variable_entry = | SectionLocalDef of constr - | SectionLocalDecl of constr + | SectionLocalAssum of constr type sticky = bool @@ -56,7 +56,7 @@ let _ = Summary.declare_summary "VARIABLE" let cache_variable (sp,((id,(d,_,_) as vd),imps)) = begin match d with (* Fails if not well-typed *) - | SectionLocalDecl ty -> Global.push_named_assum (id,ty) + | SectionLocalAssum ty -> Global.push_named_assum (id,ty) | SectionLocalDef c -> Global.push_named_def (id,c) end; Nametab.push id sp; diff --git a/library/declare.mli b/library/declare.mli index db27ccf986..5d0551486b 100644 --- a/library/declare.mli +++ b/library/declare.mli @@ -22,7 +22,7 @@ type strength = type section_variable_entry = | SectionLocalDef of constr - | SectionLocalDecl of constr + | SectionLocalAssum of constr type sticky = bool |