diff options
| author | herbelin | 2000-11-09 16:37:10 +0000 |
|---|---|---|
| committer | herbelin | 2000-11-09 16:37:10 +0000 |
| commit | 05f7dc09dea7f8ba949aeb8108f041a882fa4cf8 (patch) | |
| tree | cccf0e25701b4b8a9b995a982e64c9d495cf4bd7 /library | |
| parent | c60ee989404713617b7278ad26c285d8cea229fc (diff) | |
Renommage canonique SectionLocalDecl -> SectionLocalAssum
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@837 85f007b7-540e-0410-9357-904b9bb8a0f7
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 |