From 300293c119981054c95182a90c829058530a6b6f Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Sun, 25 Dec 2011 13:19:42 +0100
Subject: Imported Upstream version 8.3.pl3

---
 kernel/safe_typing.ml | 49 +++++++++++++++++++++++++------------------------
 1 file changed, 25 insertions(+), 24 deletions(-)

(limited to 'kernel/safe_typing.ml')

diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index dee2f5e8..4575d5bc 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: safe_typing.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
+(* $Id: safe_typing.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
 
 open Util
 open Names
@@ -40,10 +40,26 @@ type module_info =
      variant : modvariant;
      resolver : delta_resolver;
      resolver_of_param : delta_resolver;}
-      
+
 let check_label l labset =
   if Labset.mem l labset then error_existing_label l
 
+let check_labels ls senv =
+  Labset.iter (fun l -> check_label l senv) ls
+
+let labels_of_mib mib =
+  let add,get =
+    let labels = ref Labset.empty in
+    (fun id -> labels := Labset.add (label_of_id id) !labels),
+    (fun () -> !labels)
+  in
+  let visit_mip mip =
+    add mip.mind_typename;
+    Array.iter add mip.mind_consnames
+  in
+  Array.iter visit_mip mib.mind_packets;
+  get ()
+
 let set_engagement_opt oeng env =
   match oeng with
       Some eng -> set_engagement eng env
@@ -107,22 +123,6 @@ let add_constraints cst senv =
     univ = Univ.Constraint.union cst senv.univ }
 
 
-(*spiwack: functions for safe retroknowledge *)
-
-(* terms which are closed under the environnement env, i.e
-   terms which only depends on constant who are themselves closed *)
-let closed env term =
-  ContextObjectMap.is_empty (assumptions full_transparent_state env term)
-
-(* the set of safe terms in an environement any recursive set of
-   terms who are known not to prove inconsistent statement. It should
-   include at least all the closed terms. But it could contain other ones
-   like the axiom of excluded middle for instance *)
-let safe =
-  closed
-
-
-
 (* universal lifting, used for the "get" operations mostly *)
 let retroknowledge f senv =
   Environ.retroknowledge f (env_of_senv senv)
@@ -242,17 +242,16 @@ let add_mind dir l mie senv =
   if l <> label_of_id id then
     anomaly ("the label of inductive packet and its first inductive"^
 	     " type do not match");
-  check_label l senv.labset;
-    (* TODO: when we will allow reorderings we will have to verify
-       all labels *)
   let mib = translate_mind senv.env mie in
+  let labels = labels_of_mib mib in
+  check_labels labels senv.labset;
   let senv' = add_constraints mib.mind_constraints senv in
   let kn = make_mind senv.modinfo.modpath dir l in
   let env'' = Environ.add_mind kn mib senv'.env in
   kn, { old = senv'.old;
 	env = env'';
 	modinfo = senv'.modinfo;
-	labset = Labset.add l senv'.labset;  (* TODO: the same as above *)
+	labset = Labset.union labels senv'.labset;
 	revstruct = (l,SFBmind mib)::senv'.revstruct;
         univ = senv'.univ;
         engagement = senv'.engagement;
@@ -495,12 +494,14 @@ let end_module l restype senv =
 	     (canonical_mind 
 		(mind_of_delta resolver (mind_of_kn kn)))
 	   in
+	   let labels = labels_of_mib mib in
+	   check_labels labels senv.labset;
 	   let senv' = add_constraints mib.mind_constraints senv in
 	   let env'' = Environ.add_mind mind mib senv'.env in
 	     { old = senv'.old;
 	       env = env'';
 	       modinfo = senv'.modinfo;
-	       labset = Labset.add l senv'.labset;
+	       labset = Labset.union labels senv'.labset;
 	       revstruct = (l,SFBmind mib)::senv'.revstruct;
                univ = senv'.univ;
                engagement = senv'.engagement;
-- 
cgit v1.2.3