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, 59 insertions, 0 deletions

diff --git a/library/dischargedhypsmap.ml b/library/dischargedhypsmap.ml
new file mode 100644
index 000000000..5241bf035
--- /dev/null
+++ b/library/dischargedhypsmap.ml
@@ -0,0 +1,59 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+
+(* $Id$ *)
+
+open Util
+open Libnames
+open Names
+open Term
+open Reduction
+open Declarations
+open Environ
+open Inductive
+open Libobject
+open Lib
+open Nametab
+
+type discharged_hyps = section_path list
+
+let discharged_hyps_map = ref Spmap.empty
+
+let cache_discharged_hyps_map (_,(sp,hyps)) = 
+  discharged_hyps_map := Spmap.add sp hyps !discharged_hyps_map
+
+let (in_discharged_hyps_map, _) =
+  declare_object { (default_object "DISCHARGED-HYPS-MAP") with
+    cache_function = cache_discharged_hyps_map;
+    load_function = (fun _ -> cache_discharged_hyps_map);
+    export_function = (fun x -> Some x) }
+
+let set_discharged_hyps sp hyps =
+ add_anonymous_leaf (in_discharged_hyps_map (sp,hyps))
+
+let get_discharged_hyps sp =
+  try
+   Spmap.find sp !discharged_hyps_map
+  with Not_found ->
+   anomaly ("No discharged hypothesis for object " ^ string_of_path sp)
+
+(*s Registration as global tables and rollback. *)
+
+let init () =
+  discharged_hyps_map := Spmap.empty
+
+let freeze () = !discharged_hyps_map
+
+let unfreeze dhm = discharged_hyps_map := dhm
+
+let _ = 
+  Summary.declare_summary "discharged_hypothesis"
+    { Summary.freeze_function = freeze;
+      Summary.unfreeze_function = unfreeze;
+      Summary.init_function = init;
+      Summary.survive_section = true }