Renommage canonique SectionLocalDecl -> SectionLocalAssum

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@837 85f007b7-540e-0410-9357-904b9bb8a0f7

5 files changed, 8 insertions, 8 deletions

diff --git a/contrib/xml/xmlcommand.ml b/contrib/xml/xmlcommand.ml
index a321ce1ab1..ec9c3b5d2e 100644
--- a/contrib/xml/xmlcommand.ml
+++ b/contrib/xml/xmlcommand.ml
@@ -660,7 +660,7 @@ let print_object lobj id sp dn fv =
          let typ =
           match varentry with
              Declare.SectionLocalDef _ -> assert false
-           | Declare.SectionLocalDecl typ -> typ
+           | Declare.SectionLocalAssum typ -> typ
          in
           add_to_pvars (N.string_of_id id) ;
           print_variable id (T.body_of_type typ)
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
 
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 1a236c3ff7..cf980cc79b 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -84,7 +84,7 @@ let hypothesis_def_var is_refining ident n c =
         if Lib.is_section_p disch_sp then begin
 	  let t = interp_type Evd.empty (Global.env()) c in
           declare_variable (id_of_string ident)
-             (SectionLocalDecl t,n,false);
+             (SectionLocalAssum t,n,false);
 	  if is_verbose() then message (ident ^ " is assumed");
           if is_refining then 
             mSGERRNL [< 'sTR"Warning: Variable "; 'sTR ident; 
@@ -207,7 +207,7 @@ let build_recursive lnameargsardef =
            let arj = type_judgment_of_rawconstr Evd.empty env raw_arity in
 	   let arity = arj.utj_val in
            declare_variable recname
-	     (SectionLocalDecl arj.utj_val,NeverDischarge,false);
+	     (SectionLocalAssum arj.utj_val,NeverDischarge,false);
            (Environ.push_named_assum (recname,arity) env, (arity::arl)))
         (env0,[]) lnameargsardef
     with e ->
@@ -274,7 +274,7 @@ let build_corecursive lnameardef =
            let arj = type_judgment_of_rawconstr Evd.empty env0 arityc in
 	   let arity = arj.utj_val in
            declare_variable recname
-	     (SectionLocalDecl arj.utj_val,NeverDischarge,false);
+	     (SectionLocalAssum arj.utj_val,NeverDischarge,false);
            (Environ.push_named_assum (recname,arity) env, (arity::arl)))
         (env0,[]) lnameardef
     with e -> 
diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml
index 01e58b3441..a47c9effc8 100644
--- a/toplevel/discharge.ml
+++ b/toplevel/discharge.ml
@@ -139,7 +139,7 @@ let process_object oldenv sec_sp (ops,ids_to_discard,work_alist) (sp,lobj) =
 	  let newdecl =
 	    match c with
 	      | None ->
-		  SectionLocalDecl
+		  SectionLocalAssum
 		    (expmod_constr oldenv work_alist (body_of_type t))
 	      | Some body ->
 		  SectionLocalDef