Intégration des modifs de la branche mowgli :

- Simplification de strength qui est maintenant un simple drapeau Local/Global.
- Export des catégories de déclarations (Lemma/Theorem/Definition/.../
  Axiom/Parameter/..) vers les .vo (nouveau fichier library/decl_kinds.ml).
- Export des variables de section initialement associées à une déclaration
  (nouveau fichier library/dischargedhypsmap.ml).


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

1 files changed, 5 insertions, 5 deletions

diff --git a/toplevel/record.ml b/toplevel/record.ml
index 60855b2fc..909cef6d0 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1       *)
 (***********************************************************************)
 
-(* $:Id$ *)
+(* $Id$ *)
 
 open Pp
 open Util
@@ -25,7 +25,7 @@ open Astterm
 open Command
 open Inductive
 open Safe_typing
-open Nametab
+open Decl_kinds
 open Indtypes
 open Type_errors
 
@@ -178,14 +178,14 @@ let declare_projections indsp coers fields =
 		    const_entry_body = proj;
                     const_entry_type = Some projtyp;
                     const_entry_opaque = false } in
-		  declare_constant fid (DefinitionEntry cie,NeverDischarge)
+		  declare_constant fid (DefinitionEntry cie,IsDefinition)
                 with Type_errors.TypeError (ctx,te) ->
                   raise (NotDefinable (BadTypedProj (fid,ctx,te))) in
 	      let refi = ConstRef kn in
 	      let constr_fi = mkConst kn in
 	      if coe then begin
 	        let cl = Class.class_of_ref (IndRef indsp) in
-	        Class.try_add_new_coercion_with_source refi NeverDischarge cl
+	        Class.try_add_new_coercion_with_source refi Global cl
 	      end;
 	      let proj_args = (*Rel 1 refers to "x"*) paramargs@[mkRel 1] in
 	      let constr_fip = applist (constr_fi,proj_args) in
@@ -228,5 +228,5 @@ let definition_structure ((is_coe,idstruc),ps,cfs,idbuild,s) =
   let rsp = (sp,0) in (* This is ind path of idstruc *)
   let sp_projs = declare_projections rsp coers fields in
   let build = ConstructRef (rsp,1) in (* This is construct path of idbuild *)
-  if is_coe then Class.try_add_new_coercion build NeverDischarge;
+  if is_coe then Class.try_add_new_coercion build Global;
   Recordops.add_new_struc (rsp,idbuild,nparams,List.rev sp_projs)