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

9 files changed, 106 insertions, 98 deletions

diff --git a/library/declare.ml b/library/declare.ml
index 4bdc11c3..c349bef1 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: declare.ml 11282 2008-07-28 11:51:53Z msozeau $ *)
+(* $Id: declare.ml 12187 2009-06-13 19:36:59Z msozeau $ *)
 
 (** This module is about the low-level declaration of logical objects *)
 
@@ -43,7 +43,7 @@ let set_xml_declare_inductive f = xml_declare_inductive := if_xml f
 
 type section_variable_entry =
   | SectionLocalDef of constr * types option * bool (* opacity *)
-  | SectionLocalAssum of types * bool * bool (* Implicit status, Keep *)
+  | SectionLocalAssum of types * bool * identifier list (* Implicit status, Keep *)
 
 type variable_declaration = dir_path * section_variable_entry * logical_kind
 
@@ -58,7 +58,7 @@ let cache_variable ((sp,_),o) =
     | SectionLocalAssum (ty, impl, keep) ->
         let cst = Global.push_named_assum (id,ty) in
 	let impl = if impl then Lib.Implicit else Lib.Explicit in
-	let keep = if keep then Some ty else None in
+	let keep = if keep <> [] then Some (ty, keep) else None in
 	impl, true, cst, keep
     | SectionLocalDef (c,t,opaq) -> 
         let cst = Global.push_named_def (id,c,t) in
diff --git a/library/declare.mli b/library/declare.mli
index 78d3f027..2f1cd06e 100644
--- a/library/declare.mli
+++ b/library/declare.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: declare.mli 10840 2008-04-23 21:29:34Z herbelin $ i*)
+(*i $Id: declare.mli 12187 2009-06-13 19:36:59Z msozeau $ i*)
 
 (*i*)
 open Names
@@ -34,7 +34,7 @@ open Nametab
 
 type section_variable_entry =
   | SectionLocalDef of constr * types option * bool (* opacity *)
-  | SectionLocalAssum of types * bool * bool (* Implicit status, Keep *)
+  | SectionLocalAssum of types * bool * identifier list (* Implicit status, Keep list *)
 
 type variable_declaration = dir_path * section_variable_entry * logical_kind
 
diff --git a/library/declaremods.ml b/library/declaremods.ml
index 3026143b..93021384 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: declaremods.ml 11898 2009-02-10 10:52:45Z soubiran $ i*)
+(*i $Id: declaremods.ml 12204 2009-06-22 16:06:49Z soubiran $ i*)
 open Pp
 open Util
 open Names
@@ -642,29 +642,30 @@ let rec get_modtype_substobjs env = function
 	    (subst_key (map_msid msid mp) sub_alias)
 	      (map_msid msid mp)
 	| _ -> sub_alias in
-    let sub3=
+      let (subst, mbids, msid, objs) = get_modtype_substobjs env mexpr in
+      let mbid,mbids= (match mbids with
+	   | mbid::mbids -> mbid,mbids
+	   | [] -> match mexpr with
+	       | MSEident _  -> error "Application of a non-functor"
+	       | _ -> error "Application of a functor with too few arguments") in
+      let resolve =
+	Modops.resolver_of_environment farg_id farg_b mp sub_alias env in
+      let sub3=
 	if sub1 = empty_subst then
-	  update_subst sub_alias (map_mbid farg_id mp None)
+	  update_subst sub_alias (map_mbid farg_id mp (Some resolve))
 	else
-	  let sub1' = join_alias sub1 (map_mbid farg_id mp None) in
+	  let sub1' = join_alias sub1 (map_mbid farg_id mp (Some resolve)) in
 	  let sub_alias' =  update_subst sub_alias sub1' in
 	    join sub1' sub_alias'
       in
-      let sub3 = join sub3 (update_subst sub_alias (map_mbid farg_id mp None)) in
-       let (subst, mbids, msid, objs) = get_modtype_substobjs env mexpr in
-	(match mbids with
-	   | mbid::mbids ->
-               let resolve =
-		 Modops.resolver_of_environment farg_id farg_b mp sub_alias env in
-		 (* application outside the kernel, only for substitutive
-                    objects (that are all non-logical objects) *)
-		((join 
-		    (join subst sub3)
-		    (map_mbid mbid mp (Some resolve)))
-		       , mbids, msid, objs)
-	   | [] -> match mexpr with
-	       | MSEident _  -> error "Application of a non-functor"
-	       | _ -> error "Application of a functor with too few arguments")
+      let sub3 = join sub3 
+	(update_subst sub_alias (map_mbid farg_id mp (Some resolve))) in
+	(* application outside the kernel, only for substitutive
+           objects (that are all non-logical objects) *)
+	((join 
+	    (join subst sub3)
+	    (map_mbid mbid mp (Some resolve)))
+	   , mbids, msid, objs)
   | MSEapply (_,mexpr) ->
       Modops.error_application_to_not_path mexpr
 
@@ -948,30 +949,32 @@ let rec get_module_substobjs env = function
 	    (subst_key (map_msid msid mp) sub_alias)
 	      (map_msid msid mp)
 	| _ -> sub_alias in
-
+      let (subst, mbids, msid, objs) = get_module_substobjs env mexpr in
+      let mbid,mbids = 
+	(match mbids with
+	   | mbid::mbids ->mbid,mbids
+	       
+	   | [] -> match mexpr with
+	       | MSEident _  -> error "Application of a non-functor"
+	       | _ -> error "Application of a functor with too few arguments") in
+      let resolve =
+	Modops.resolver_of_environment farg_id farg_b mp sub_alias env in
       let sub3=
 	if sub1 = empty_subst then
-	  update_subst sub_alias (map_mbid farg_id mp None)
+	  update_subst sub_alias (map_mbid farg_id mp (Some resolve))
 	else
-	  let sub1' = join_alias sub1 (map_mbid farg_id mp None) in
+	  let sub1' = join_alias sub1 (map_mbid farg_id mp (Some resolve)) in
 	  let sub_alias' =  update_subst sub_alias sub1' in
-	    join sub1' sub_alias'
+		     join sub1' sub_alias'
       in
-      let sub3 = join sub3 (update_subst sub_alias (map_mbid farg_id mp None)) in
-      let (subst, mbids, msid, objs) = get_module_substobjs env mexpr in
-	(match mbids with
-	   | mbid::mbids ->
-               let resolve =
-		 Modops.resolver_of_environment farg_id farg_b mp sub_alias env in
-		 (* application outside the kernel, only for substitutive
-                    objects (that are all non-logical objects) *)
-		((join 
-		    (join subst sub3)
-		       (map_mbid mbid mp (Some resolve)))
-		       , mbids, msid, objs)
-	   | [] -> match mexpr with
-	       | MSEident _  -> error "Application of a non-functor"
-	       | _ -> error "Application of a functor with too few arguments")
+      let sub3 = join sub3 (update_subst sub_alias 
+			      (map_mbid farg_id mp (Some resolve))) in
+	(* application outside the kernel, only for substitutive
+           objects (that are all non-logical objects) *)
+	((join 
+	    (join subst sub3)
+	    (map_mbid mbid mp (Some resolve)))
+	   , mbids, msid, objs)
   | MSEapply (_,mexpr) ->
       Modops.error_application_to_not_path mexpr
   | MSEwith (mty, With_Definition _) -> get_module_substobjs env mty
@@ -1061,12 +1064,9 @@ let rec update_include (sub,mbids,msid,objs) =
     | (id,obj)::tail ->
 	if object_tag obj = "INCLUDE" then
 	  let ((me,is_mod),substobjs,substituted) = out_include obj in
-	    if not (is_mod) then
-	      let substobjs' = update_include substobjs in
-                (id, in_include ((me,true),substobjs',substituted))::
-		  (replace_include tail)
-	    else
-		  (id,obj)::(replace_include tail)
+	  let substobjs' = update_include substobjs in
+            (id, in_include ((me,true),substobjs',substituted))::
+	      (replace_include tail)
 	else
 	  (id,obj)::(replace_include tail)
   in
@@ -1142,7 +1142,7 @@ let declare_module interp_modtype interp_modexpr id args mty_o mexpr_o =
       | _ ->
 	  let dir,mp = dir_of_sp (Lib.make_path id), mp_of_kn (Lib.make_kn id) in
 	  let (sub,mbids,msid,objs) = substobjs in
-	  let sub' = subst_key (map_msid msid mp) sub in
+	  let sub' = join_alias (subst_key (map_msid msid mp) sub) (map_msid msid mp) in
 	  let substobjs = (join sub sub',mbids,msid,objs) in
 	  let substituted = subst_substobjs dir mp substobjs in
 	    ignore (add_leaf
diff --git a/library/impargs.ml b/library/impargs.ml
index 2b2c607c..14f88728 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: impargs.ml 11576 2008-11-10 19:13:15Z msozeau $ *)
+(* $Id: impargs.ml 12187 2009-06-13 19:36:59Z msozeau $ *)
 
 open Util
 open Names
@@ -26,8 +26,7 @@ open Termops
 (*s Flags governing the computation of implicit arguments *)
 
 type implicits_flags = {
-  main : bool;
-  manual : bool;                     (* automatic or manual only *)
+  auto : bool;                     (* automatic or manual only *)
   strict : bool;                   (* true = strict *)
   strongly_strict : bool;            (* true = strongly strict *)
   reversible_pattern : bool;
@@ -38,8 +37,7 @@ type implicits_flags = {
 (* les implicites sont stricts par défaut en v8 *)
 
 let implicit_args = ref { 
-  main = false;
-  manual = false;
+  auto = false;
   strict = true;
   strongly_strict = false;
   reversible_pattern = false;
@@ -48,11 +46,7 @@ let implicit_args = ref {
 }
 
 let make_implicit_args flag =
-  implicit_args := { !implicit_args with main = flag }
-
-let make_manual_implicit_args flag =
-  implicit_args := { !implicit_args with main = if flag then true else !implicit_args.main;
-    manual = flag }
+  implicit_args := { !implicit_args with auto = flag }
 
 let make_strict_implicit_args flag =
   implicit_args := { !implicit_args with strict = flag }
@@ -69,9 +63,7 @@ let make_contextual_implicit_args flag =
 let make_maximal_implicit_args flag =
   implicit_args := { !implicit_args with maximal = flag }
 
-let is_implicit_args () = !implicit_args.main
-let is_manual_implicit_args () = !implicit_args.manual
-let is_auto_implicit_args () = !implicit_args.main && not (is_manual_implicit_args ())
+let is_implicit_args () = !implicit_args.auto
 let is_strict_implicit_args () = !implicit_args.strict
 let is_strongly_strict_implicit_args () = !implicit_args.strongly_strict
 let is_reversible_pattern_implicit_args () = !implicit_args.reversible_pattern
@@ -316,10 +308,10 @@ let const v _ = v
 let compute_implicits_auto env f manual t =
   match manual with
   | [] -> 
-      let l = compute_implicits_flags env f false t in
-	if f.manual then List.map (const None) l
-	else prepare_implicits f l
-  | _ -> compute_manual_implicits env f t (not f.manual) manual
+      if not f.auto then []
+      else let l = compute_implicits_flags env f false t in
+	     prepare_implicits f l
+  | _ -> compute_manual_implicits env f t f.auto manual
 	
 let compute_implicits env t = compute_implicits_auto env !implicit_args [] t
 
@@ -523,7 +515,7 @@ let rebuild_implicits (req,l) =
       | ImplManual m -> 
 	  let oldimpls = snd (List.hd l) in
 	  let auto = 
-	    if flags.main then
+	    if flags.auto then
 	      let newimpls = compute_global_implicits flags [] ref in
 		merge_impls oldimpls newimpls
 	    else oldimpls
@@ -549,32 +541,30 @@ let declare_implicits_gen req flags ref =
   add_anonymous_leaf (inImplicits (req,[ref,imps]))
 
 let declare_implicits local ref =
-  let flags = { !implicit_args with main = true } in
+  let flags = { !implicit_args with auto = true } in
   let req = 
     if local then ImplLocal else ImplInteractive(ref,flags,ImplAuto) in
-  declare_implicits_gen req flags ref
-
+    declare_implicits_gen req flags ref
+      
 let declare_var_implicits id =
-  if !implicit_args.main then
-    declare_implicits_gen ImplLocal !implicit_args (VarRef id)
+  let flags = !implicit_args in
+    declare_implicits_gen ImplLocal flags (VarRef id)
 
 let declare_constant_implicits con =
-  if !implicit_args.main then
-    let flags = !implicit_args in
+  let flags = !implicit_args in
     declare_implicits_gen (ImplConstant (con,flags)) flags (ConstRef con)
 
 let declare_mib_implicits kn =
-  if !implicit_args.main then
-    let flags = !implicit_args in
-    let imps = array_map_to_list
-      (fun (ind,cstrs) -> ind::(Array.to_list cstrs))
-      (compute_mib_implicits flags [] kn) in
+  let flags = !implicit_args in
+  let imps = array_map_to_list
+    (fun (ind,cstrs) -> ind::(Array.to_list cstrs))
+    (compute_mib_implicits flags [] kn) in
     add_anonymous_leaf
       (inImplicits (ImplMutualInductive (kn,flags),List.flatten imps))
-
+      
 (* Declare manual implicits *)
 type manual_explicitation = Topconstr.explicitation * (bool * bool) 
-
+  
 let compute_implicits_with_manual env typ enriching l = 
   compute_manual_implicits env !implicit_args typ enriching l
 
@@ -582,7 +572,7 @@ let declare_manual_implicits local ref ?enriching l =
   let flags = !implicit_args in
   let env = Global.env () in
   let t = Global.type_of_global ref in
-  let enriching = Option.default (is_auto_implicit_args ()) enriching in
+  let enriching = Option.default flags.auto enriching in
   let l' = compute_manual_implicits env flags t enriching l in
   let req =
     if local or isVarRef ref then ImplLocal
diff --git a/library/impargs.mli b/library/impargs.mli
index a363effa..c1f119e6 100644
--- a/library/impargs.mli
+++ b/library/impargs.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: impargs.mli 11576 2008-11-10 19:13:15Z msozeau $ i*)
+(*i $Id: impargs.mli 12187 2009-06-13 19:36:59Z msozeau $ i*)
 
 (*i*)
 open Names
@@ -20,7 +20,6 @@ open Nametab
     are outside the kernel, which knows nothing about implicit arguments. *)
 
 val make_implicit_args : bool -> unit
-val make_manual_implicit_args : bool -> unit
 val make_strict_implicit_args : bool -> unit
 val make_strongly_strict_implicit_args : bool -> unit
 val make_reversible_pattern_implicit_args : bool -> unit
@@ -28,7 +27,6 @@ val make_contextual_implicit_args : bool -> unit
 val make_maximal_implicit_args : bool -> unit
 
 val is_implicit_args : unit -> bool
-val is_manual_implicit_args : unit -> bool
 val is_strict_implicit_args : unit -> bool
 val is_strongly_strict_implicit_args : unit -> bool
 val is_reversible_pattern_implicit_args : unit -> bool
diff --git a/library/lib.ml b/library/lib.ml
index 88bcd0b8..4a124cec 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: lib.ml 11784 2009-01-14 11:36:32Z herbelin $ *)
+(* $Id: lib.ml 12187 2009-06-13 19:36:59Z msozeau $ *)
 
 open Pp
 open Util
@@ -452,7 +452,7 @@ type variable_context = variable_info list
 type abstr_list = variable_context Names.Cmap.t * variable_context Names.KNmap.t
 
 let sectab =
-  ref ([] : ((Names.identifier * binding_kind * Term.types option) list * Cooking.work_list * abstr_list) list)
+  ref ([] : ((Names.identifier * binding_kind * (Term.types * Names.identifier list) option) list * Cooking.work_list * abstr_list) list)
 
 let add_section () =
   sectab := ([],(Names.Cmap.empty,Names.KNmap.empty),(Names.Cmap.empty,Names.KNmap.empty)) :: !sectab
@@ -460,13 +460,19 @@ let add_section () =
 let add_section_variable id impl keep =
   match !sectab with
     | [] -> () (* because (Co-)Fixpoint temporarily uses local vars *)
-    | (vars,repl,abs)::sl -> sectab := ((id,impl,keep)::vars,repl,abs)::sl
+    | (vars,repl,abs)::sl ->
+	sectab := ((id,impl,keep)::vars,repl,abs)::sl
 
-let rec extract_hyps = function
-  | ((id,impl,keep)::idl,(id',b,t)::hyps) when id=id' -> (id',impl,b,t) :: extract_hyps (idl,hyps)
-  | ((id,impl,Some ty)::idl,hyps) -> (id,impl,None,ty) :: extract_hyps (idl,hyps)
-  | (id::idl,hyps) -> extract_hyps (idl,hyps)
-  | [], _ -> []
+let extract_hyps (secs,ohyps) =
+  let rec aux = function
+    | ((id,impl,keep)::idl,(id',b,t)::hyps) when id=id' -> (id',impl,b,t) :: aux (idl,hyps)
+    | ((id,impl,Some (ty,keep))::idl,hyps) -> 
+	if List.exists (fun (id,_,_) -> List.mem id keep) ohyps then
+	  (id,impl,None,ty) :: aux (idl,hyps)
+	else aux (idl,hyps)
+    | (id::idl,hyps) -> aux (idl,hyps)
+    | [], _ -> []
+  in aux (secs,ohyps)
 
 let instance_from_variable_context sign =
   let rec inst_rec = function
diff --git a/library/lib.mli b/library/lib.mli
index 23af7c17..dacfed59 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: lib.mli 11671 2008-12-12 12:43:03Z herbelin $ i*)
+(*i $Id: lib.mli 12187 2009-06-13 19:36:59Z msozeau $ i*)
 
 
 (*s This module provides a general mechanism to keep a trace of all operations
@@ -182,7 +182,9 @@ val section_segment_of_mutual_inductive: Names.mutual_inductive -> variable_cont
 val section_instance : Libnames.global_reference -> Names.identifier array
 val is_in_section : Libnames.global_reference -> bool
 
-val add_section_variable : Names.identifier -> binding_kind -> Term.types option -> unit
+val add_section_variable : Names.identifier -> binding_kind -> 
+  (Term.types * Names.identifier list) option -> unit
+
 val add_section_constant : Names.constant -> Sign.named_context -> unit
 val add_section_kn : Names.kernel_name -> Sign.named_context -> unit
 val replacement_context : unit ->
diff --git a/library/states.ml b/library/states.ml
index 7f7fef47..c81f9614 100644
--- a/library/states.ml
+++ b/library/states.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: states.ml 11313 2008-08-07 11:15:03Z barras $ *)
+(* $Id: states.ml 12080 2009-04-11 16:56:20Z herbelin $ *)
 
 open System
 
@@ -35,3 +35,10 @@ let with_heavy_rollback f x =
     f x
   with reraise ->
     (unfreeze st; raise reraise)
+
+let with_state_protection f x =
+  let st = freeze () in
+  try 
+    let a = f x in unfreeze st; a
+  with reraise ->
+    (unfreeze st; raise reraise)
diff --git a/library/states.mli b/library/states.mli
index eff046ef..210e06b2 100644
--- a/library/states.mli
+++ b/library/states.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: states.mli 5920 2004-07-16 20:01:26Z herbelin $ i*)
+(*i $Id: states.mli 12080 2009-04-11 16:56:20Z herbelin $ i*)
 
 (*s States of the system. In that module, we provide functions to get
   and set the state of the whole system. Internally, it is done by
@@ -26,4 +26,9 @@ val unfreeze : state -> unit
 
 val with_heavy_rollback : ('a -> 'b) -> 'a -> 'b
 
+(*s [with_state_protection f x] applies [f] to [x] and restores the
+  state of the whole system as it was before the evaluation of f *)
+
+val with_state_protection : ('a -> 'b) -> 'a -> 'b
+