nouveau discharge fait par le noyau; plus de recettes dans les corps des constantes

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

4 files changed, 34 insertions, 17 deletions

diff --git a/library/declare.ml b/library/declare.ml
index b46cf0e581..84cc2e5751 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -110,24 +110,31 @@ let declare_parameter id c =
 
 (* Constants. *)
 
-type constant_declaration = constant_entry * strength
+type constant_declaration_type =
+  | ConstantEntry  of constant_entry
+  | ConstantRecipe of Cooking.recipe
 
-let csttab = ref (Spmap.empty : constant_declaration Spmap.t)
+type constant_declaration = constant_declaration_type * strength
+
+let csttab = ref (Spmap.empty : strength Spmap.t)
 
 let _ = Summary.declare_summary "CONSTANT"
 	  { Summary.freeze_function = (fun () -> !csttab);
 	    Summary.unfreeze_function = (fun ft -> csttab := ft);
 	    Summary.init_function = (fun () -> csttab := Spmap.empty) }
 
-let cache_constant (sp,((ce,_) as cd,imps)) =
-  Global.add_constant sp ce;
+let cache_constant (sp,((cdt,stre),imps)) =
+  begin match cdt with 
+    | ConstantEntry ce -> Global.add_constant sp ce
+    | ConstantRecipe r -> Global.add_discharged_constant sp r
+  end;
   Nametab.push (basename sp) sp;
   if imps then declare_constant_implicits sp;
-  csttab := Spmap.add sp cd !csttab
+  csttab := Spmap.add sp stre !csttab
 
-let load_constant (sp,((ce,_) as cd,imps)) =
+let load_constant (sp,((ce,stre),imps)) =
   if imps then declare_constant_implicits sp;
-  csttab := Spmap.add sp cd !csttab
+  csttab := Spmap.add sp stre !csttab
 
 let open_constant (sp,_) =
   Nametab.push (basename sp) sp
@@ -192,8 +199,7 @@ let declare_mind mie =
 let is_constant sp = 
   try let _ = Global.lookup_constant sp in true with Not_found -> false
 
-let constant_strength sp = 
-  let (_,stre) = Spmap.find sp !csttab in stre
+let constant_strength sp = Spmap.find sp !csttab
 
 let constant_or_parameter_strength sp =
   try constant_strength sp with Not_found -> NeverDischarge
@@ -359,7 +365,7 @@ let declare_eliminations sp i =
   let mindstr = string_of_id (mis_typename mispec) in
   let declare na c =
     declare_constant (id_of_string na)
-      ({ const_entry_body = Cooked c; const_entry_type = None }, 
+      (ConstantEntry { const_entry_body = c; const_entry_type = None }, 
        NeverDischarge);
     if Options.is_verbose() then pPNL [< 'sTR na; 'sTR " is defined" >]
   in
diff --git a/library/declare.mli b/library/declare.mli
index cd931d94d6..b8e45bdea6 100644
--- a/library/declare.mli
+++ b/library/declare.mli
@@ -27,9 +27,15 @@ type section_variable_entry =
 type sticky = bool
 
 type variable_declaration = section_variable_entry * strength * sticky
+
 val declare_variable : identifier -> variable_declaration -> unit
 
-type constant_declaration = constant_entry * strength
+type constant_declaration_type =
+  | ConstantEntry  of constant_entry
+  | ConstantRecipe of Cooking.recipe
+
+type constant_declaration = constant_declaration_type * strength
+
 val declare_constant : identifier -> constant_declaration -> unit
 
 val declare_parameter : identifier -> constr -> unit
diff --git a/library/global.ml b/library/global.ml
index 7b69ca0a85..6a2dfe145e 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -33,21 +33,23 @@ let named_context () = named_context !global_env
 let push_named_def idc = global_env := push_named_def idc !global_env
 let push_named_assum idc = global_env := push_named_assum idc !global_env
 
-let add_constant sp ce = global_env := add_constant sp ce !global_env
 let add_parameter sp c = global_env := add_parameter sp c !global_env
+let add_constant sp ce = global_env := add_constant sp ce !global_env
+let add_discharged_constant sp r = 
+  global_env := add_discharged_constant sp r !global_env
 let add_mind sp mie = global_env := add_mind sp mie !global_env
 let add_constraints c = global_env := add_constraints c !global_env
 
 let pop_named_decls ids = global_env := pop_named_decls ids !global_env
 
 let lookup_named id = lookup_named id !global_env
-(*
-let lookup_rel n = lookup_rel n !global_env
-*)
 let lookup_constant sp = lookup_constant sp !global_env
 let lookup_mind sp = lookup_mind sp !global_env
 let lookup_mind_specif c = lookup_mind_specif c !global_env
 
+let set_opaque sp = set_opaque !global_env sp
+let set_transparent sp = set_transparent !global_env sp
+
 let export s = export !global_env s
 let import cenv = global_env := import cenv !global_env
 
diff --git a/library/global.mli b/library/global.mli
index a59c998231..0dcaef62a1 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -26,19 +26,22 @@ val named_context : unit -> named_context
 val push_named_assum : identifier * constr -> unit
 val push_named_def : identifier * constr -> unit
 
-val add_constant : section_path -> constant_entry -> unit
 val add_parameter : section_path -> constr -> unit
+val add_constant : section_path -> constant_entry -> unit
+val add_discharged_constant : section_path -> Cooking.recipe -> unit
 val add_mind : section_path -> mutual_inductive_entry -> unit
 val add_constraints : constraints -> unit
 
 val pop_named_decls : identifier list -> unit
 
 val lookup_named : identifier -> constr option * types
-(*i val lookup_rel : int -> name * types i*)
 val lookup_constant : section_path -> constant_body
 val lookup_mind : section_path -> mutual_inductive_body
 val lookup_mind_specif : inductive -> inductive_instance
 
+val set_opaque : section_path -> unit
+val set_transparent : section_path -> unit
+
 val export : string -> compiled_env
 val import : compiled_env -> unit