Imported Upstream version 8.2.pl1+dfsgupstream/8.2.pl1+dfsg

5 files changed, 48 insertions, 33 deletions

diff --git a/kernel/environ.ml b/kernel/environ.ml
index 86e02623..cd4efe27 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: environ.ml 11309 2008-08-06 10:30:35Z herbelin $ *)
+(* $Id: environ.ml 12187 2009-06-13 19:36:59Z msozeau $ *)
 
 open Util
 open Names
@@ -554,7 +554,7 @@ fun env field value ->
 type context_object =
   | Variable of identifier (* A section variable or a Let definition *)
   | Axiom of constant      (* An axiom or a constant. *)
-
+  | Opaque of constant     (* An opaque constant. *)
 
 (* Defines a set of [assumption] *)
 module OrderedContextObject = 
@@ -566,15 +566,19 @@ struct
       | Axiom k1 , Axiom k2 -> Pervasives.compare k1 k2
 	          (* spiwack: it would probably be cleaner
 		     to provide a [kn_ord] function *)
+      | Opaque k1 , Opaque k2 -> Pervasives.compare k1 k2
       | Variable _ , Axiom _ -> -1
       | Axiom _ , Variable _ -> 1
+      | Opaque _ , _ -> -1
+      | _, Opaque _ -> 1
 end
 
 module ContextObjectSet = Set.Make (OrderedContextObject)
 module ContextObjectMap = Map.Make (OrderedContextObject)
 
 
-let assumptions (* t env *) =   
+let assumptions ?(add_opaque=false) st (* t env *) =
+  let (idts,knst) = st in
   (* Infix definition for chaining function that accumulate
      on a and a ContextObjectSet, ContextObjectMap.  *)
   let ( ** ) f1 f2 s m = let (s',m') = f1 s m in f2 s' m' in
@@ -650,16 +654,26 @@ let assumptions (* t env *) =
 
   and add_kn kn env s acc =
     let cb = lookup_constant kn env in
-    match cb.Declarations.const_body with
-    | None -> 
-	let ctype = 
-	  match cb.Declarations.const_type with
-	  | PolymorphicArity (ctx,a) -> mkArity (ctx, Type a.poly_level)
-	  | NonPolymorphicType t -> t
-	in
-	(s,ContextObjectMap.add (Axiom kn) ctype acc)
-    | Some body -> aux (Declarations.force body) env s acc
-
+    let do_type cst =
+      let ctype =
+	match cb.Declarations.const_type with
+	| PolymorphicArity (ctx,a) -> mkArity (ctx, Type a.poly_level)
+	| NonPolymorphicType t -> t
+      in
+	(s,ContextObjectMap.add cst ctype acc)
+    in
+    let (s,acc) =
+      if cb.Declarations.const_body <> None
+	&& (cb.Declarations.const_opaque || not (Cpred.mem kn knst))
+	&& add_opaque 
+      then
+	do_type (Opaque kn)
+      else (s,acc)
+    in
+      match cb.Declarations.const_body with
+      | None -> do_type (Axiom kn)
+      | Some body -> aux (Declarations.force body) env s acc
+	  
   and aux_memoize_kn kn env =
     try_and_go (Axiom kn) (add_kn kn env)
  in
diff --git a/kernel/environ.mli b/kernel/environ.mli
index 97e19782..b68123f6 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: environ.mli 11309 2008-08-06 10:30:35Z herbelin $ i*)
+(*i $Id: environ.mli 12187 2009-06-13 19:36:59Z msozeau $ i*)
 
 (*i*)
 open Names
@@ -244,13 +244,14 @@ val register : env -> field -> Retroknowledge.entry -> env
 type context_object =
   | Variable of identifier (* A section variable or a Let definition *)
   | Axiom of constant      (* An axiom or a constant. *)
+  | Opaque of constant     (* An opaque constant. *)
 
 (* AssumptionSet.t is a set of [assumption] *)
 module OrderedContextObject :  Set.OrderedType with type t = context_object
 module ContextObjectMap : Map.S with type key = context_object
 
-(* collects all the assumptions on which a term relies (together with
-   their type *)
-val assumptions : constr -> env -> Term.types ContextObjectMap.t
+(* collects all the assumptions (optionally including opaque definitions) 
+   on which a term relies (together with their type) *)
+val assumptions : ?add_opaque:bool -> transparent_state -> constr -> env -> Term.types ContextObjectMap.t
 
 
diff --git a/kernel/mod_subst.ml b/kernel/mod_subst.ml
index ab4b8e47..9a76922b 100644
--- a/kernel/mod_subst.ml
+++ b/kernel/mod_subst.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: mod_subst.ml 10849 2008-04-25 15:55:16Z soubiran $ *)
+(* $Id: mod_subst.ml 11924 2009-02-13 13:51:54Z soubiran $ *)
 
 open Pp
 open Util
@@ -250,11 +250,11 @@ let join (subst1 : substitution) (subst2 : substitution) =
       try
 	let res =
 	  match resolve with
-              Some res -> res
-	    | None ->
+	    |None -> begin
 		match resolve' with
 		    None -> raise BothSubstitutionsAreIdentitySubstitutions
-		  | Some res -> raise (ChangeDomain res)
+		  | Some res -> raise (ChangeDomain res) end
+	    | Some res -> res
 	in
 	  Some
 	    (List.map
@@ -356,23 +356,23 @@ let update_subst subst1 subst2 =
 	| MPI mp -> mp
     in
    match mp with 
-     | MPbound mbid ->  ((MBI mbid),newmp)::l
-     | MPself msid ->  ((MSI msid),newmp)::l
-     | _ ->   ((MPI mp),newmp)::l
+     | MPbound mbid ->  ((MBI mbid),newmp,resolve)::l
+     | MPself msid ->  ((MSI msid),newmp,resolve)::l
+     | _ ->   ((MPI mp),newmp,resolve)::l
   in 
   let subst_mbi = Umap.fold subst_inv subst2 [] in
   let alias_subst key (mp,resolve) sub=
     let newsetkey = 
       match key with
 	| MPI mp1 -> 
-	    let compute_set_newkey l (k,mp') = 
+	    let compute_set_newkey l (k,mp',resolve) = 
 	      let mp_from_key = match k with
 		  	| MBI msid -> MPbound msid
 			| MSI msid -> MPself msid
 			| MPI mp -> mp
 	      in
 	      let new_mp1 = replace_mp_in_mp mp_from_key mp' mp1 in
-		if new_mp1 == mp1 then l else (MPI new_mp1)::l
+		if new_mp1 == mp1 then l else (MPI new_mp1,resolve)::l
 	    in
 	    begin
 	      match List.fold_left compute_set_newkey [] subst_mbi with
@@ -384,7 +384,7 @@ let update_subst subst1 subst2 =
       match newsetkey with
 	| None -> sub
 	| Some l -> 
-	    List.fold_left (fun s k -> Umap.add k (mp,resolve) s)
+	    List.fold_left (fun s (k,r) -> Umap.add k (mp,r) s)
 	      sub l
   in
     Umap.fold alias_subst subst1 empty_subst
diff --git a/kernel/modops.ml b/kernel/modops.ml
index 25a11c69..949a7402 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: modops.ml 11514 2008-10-28 13:39:02Z soubiran $ i*)
+(*i $Id: modops.ml 11923 2009-02-13 12:20:27Z soubiran $ i*)
 
 (*i*)
 open Util
@@ -272,9 +272,9 @@ let rec eval_struct env = function
 	      (subst_key (map_msid msid mp) sub_alias)
 	      (map_msid msid mp)
 	| _ -> sub_alias in
-      let sub_alias1 = update_subst sub_alias 
-	(map_mbid farg_id mp (None)) in
-      let resolve = resolver_of_environment farg_id farg_b mp sub_alias env in
+    let resolve = resolver_of_environment farg_id farg_b mp sub_alias env in  
+    let sub_alias1 = update_subst sub_alias 
+	(map_mbid farg_id mp (Some resolve)) in
 	eval_struct env (subst_struct_expr 
 			   (join sub_alias1 
 			      (map_mbid farg_id mp (Some resolve))) fbody_b)
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index fbb05a2d..7a2db86b 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: safe_typing.ml 11453 2008-10-15 14:42:34Z soubiran $ *)
+(* $Id: safe_typing.ml 12187 2009-06-13 19:36:59Z msozeau $ *)
 
 open Util
 open Names
@@ -113,7 +113,7 @@ let add_constraints cst senv =
 (* 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 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