From 05f7dc09dea7f8ba949aeb8108f041a882fa4cf8 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Thu, 9 Nov 2000 16:37:10 +0000
Subject: Renommage canonique SectionLocalDecl -> SectionLocalAssum

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@837 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 library/declare.ml  | 4 ++--
 library/declare.mli | 2 +-
 2 files changed, 3 insertions(+), 3 deletions(-)

(limited to 'library')

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
 
-- 
cgit v1.2.3