From db76a192ec07bf71b0f0bf648f66d3487c27f1b3 Mon Sep 17 00:00:00 2001
From: filliatr
Date: Wed, 1 Dec 1999 10:52:56 +0000
Subject: make_strength / reset_library

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

diff --git a/library/declare.ml b/library/declare.ml
index 9a32c1d461..bcfc312dff 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -18,6 +18,10 @@ type strength =
   | DischargeAt of section_path 
   | NeverDischarge
 
+let make_strength = function
+  | [] -> NeverDischarge
+  | l  -> DischargeAt (sp_of_wd l)
+
 (* Variables. *)
 
 let cache_variable (_,obj) = 
diff --git a/library/declare.mli b/library/declare.mli
index c32ce46ac8..8a75172b63 100644
--- a/library/declare.mli
+++ b/library/declare.mli
@@ -32,6 +32,7 @@ val declare_eliminations : section_path -> unit
 
 val declare_syntax_constant : identifier -> constr -> unit
 
+val make_strength : string list -> strength
 
 (*s Corresponding test and access functions. *)
 
diff --git a/library/lib.ml b/library/lib.ml
index 46a2833f57..ea81207871 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -192,5 +192,7 @@ let unfreeze stk =
 let init () =
   lib_stk := [];
   add_frozen_state ();
-  path_prefix := []
+  path_prefix := [];
+  init_summaries()
+
 
-- 
cgit v1.2.3