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

7 files changed, 52 insertions, 37 deletions

diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index 04945040..1a1640a4 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -7,7 +7,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: classes.ml 11800 2009-01-18 18:34:15Z msozeau $ i*)
+(*i $Id: classes.ml 12187 2009-06-13 19:36:59Z msozeau $ i*)
 
 (*i*)
 open Names
@@ -264,6 +264,14 @@ let named_of_rel_context l =
       l ([], [])
   in ctx
 
+let push_named_context = List.fold_right push_named
+
+let rec list_filter_map f = function
+  | [] -> []
+  | hd :: tl -> match f hd with
+    | None -> list_filter_map f tl
+    | Some x -> x :: list_filter_map f tl
+
 let context ?(hook=fun _ -> ()) l =
   let env = Global.env() in
   let evars = ref (Evd.create_evar_defs Evd.empty) in
@@ -274,6 +282,14 @@ let context ?(hook=fun _ -> ()) l =
   let ctx = try named_of_rel_context fullctx with _ -> 
     error "Anonymous variables not allowed in contexts."
   in
+  let env = push_named_context ctx env in
+  let keeps = 
+    List.fold_left (fun acc (id,_,t) ->
+      match class_of_constr t with
+      | None -> acc
+      | Some _ -> List.map pi1 (keep_hyps env (Idset.singleton id)) :: acc)
+      [] ctx
+  in
     List.iter (function (id,_,t) -> 
       if Lib.is_modtype () then 
 	let cst = Declare.declare_internal_constant id
@@ -285,10 +301,14 @@ let context ?(hook=fun _ -> ()) l =
 		hook (ConstRef cst)
 	    | None -> ()
       else (
-	let impl = List.exists (fun (x,_) -> match x with ExplByPos (_, Some id') -> id = id' | _ -> false) impls
+	let impl = List.exists (fun (x,_) -> 
+	  match x with ExplByPos (_, Some id') -> id = id' | _ -> false) impls 
+	and keep = 
+	  let l = list_filter_map (fun ids -> if List.mem id ids then Some ids else None) keeps in
+	    List.concat l
 	in
 	  Command.declare_one_assumption false (Local (* global *), Definitional) t
-	    [] impl (* implicit *) true (* always kept *) false (* inline *) (dummy_loc, id);
+	    [] impl (* implicit *) keep (* always kept *) false (* inline *) (dummy_loc, id);
 	  match class_of_constr t with
 	  | None -> ()
 	  | Some tc -> hook (VarRef id)))
diff --git a/toplevel/command.ml b/toplevel/command.ml
index b50c9bbd..05a22829 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: command.ml 11745 2009-01-04 18:43:08Z herbelin $ *)
+(* $Id: command.ml 12187 2009-06-13 19:36:59Z msozeau $ *)
 
 open Pp
 open Util
@@ -546,7 +546,7 @@ let interp_mutual paramsl indl notations finite =
   let mldatas = List.map2 (mk_mltype_data evdref env_params params) arities indnames in
 
   let constructors =
-    States.with_heavy_rollback (fun () -> 
+    States.with_state_protection (fun () -> 
      (* Temporary declaration of notations and scopes *)
      List.iter (declare_interning_data impls) notations;
      (* Interpret the constructor types *)
@@ -851,7 +851,7 @@ let interp_recursive fixkind l boxed =
 
   (* Interp bodies with rollback because temp use of notations/implicit *)
   let fixdefs = 
-    States.with_heavy_rollback (fun () -> 
+    States.with_state_protection (fun () -> 
       List.iter (declare_interning_data impls) notations;
       list_map3 (interp_fix_body evdref env_rec impls) fixctxs fixl fixccls)
       () in
@@ -1012,16 +1012,18 @@ let build_combined_scheme name schemes =
     let (ctx, arity) = decompose_prod ty in
     let (_, last) = List.hd ctx in
       match kind_of_term last with
-	| App (ind, args) -> ctx, destInd ind, Array.length args
+	| App (ind, args) -> 
+	    let ind = destInd ind in
+	    let (_,spec) = Inductive.lookup_mind_specif env ind in
+	      ctx, ind, spec.mind_nrealargs
 	| _ -> ctx, destInd last, 0
   in
   let defs =  
     List.map (fun x -> 
 		let refe = Ident x in
 		let qualid = qualid_of_reference refe in
-		let cst = try 
-                    Nametab.locate_constant (snd qualid) 
-                with Not_found -> error ((string_of_qualid (snd qualid))^" is not declared.")
+		let cst = try Nametab.locate_constant (snd qualid) 
+                  with Not_found -> error ((string_of_qualid (snd qualid))^" is not declared.")
                 in
 		let ty = Typeops.type_of_constant env cst in
 		  qualid, cst, ty)
@@ -1087,9 +1089,9 @@ let save_remaining_recthms (local,kind) body opaq i (id,(t_i,imps)) =
   | None ->
       (match local with
       | Local ->
-          let impl=false and keep=false in (* copy values from Vernacentries *)
+          let impl=false in (* copy values from Vernacentries *)
           let k = IsAssumption Conjectural in
-          let c = SectionLocalAssum (t_i,impl,keep) in
+          let c = SectionLocalAssum (t_i,impl,[]) in
 	  let _ = declare_variable id (Lib.cwd(),c,k) in
           (Local,VarRef id,imps)
       | Global ->
@@ -1123,9 +1125,9 @@ let look_for_mutual_statements thms =
     let n = List.length thms in
     let inds = List.map (fun (id,(t,_) as x) -> 
       let (hyps,ccl) = Sign.decompose_prod_assum t in
-      let whnf_hyp_hds = map_rel_context_with_binders
-        (fun i c -> fst (whd_betadeltaiota_stack (Global.env()) Evd.empty (lift i c)))
-        hyps in
+      let whnf_hyp_hds = fold_map_rel_context
+        (fun env c -> fst (whd_betadeltaiota_stack env Evd.empty c))
+	(Global.env()) hyps in
       let ind_hyps =
         List.flatten (list_map_i (fun i (_,b,t) ->
           match kind_of_term t with
diff --git a/toplevel/command.mli b/toplevel/command.mli
index b42fafd0..36399029 100644
--- a/toplevel/command.mli
+++ b/toplevel/command.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: command.mli 11745 2009-01-04 18:43:08Z herbelin $ i*)
+(*i $Id: command.mli 12187 2009-06-13 19:36:59Z msozeau $ i*)
 
 (*i*)
 open Util
@@ -45,13 +45,13 @@ val syntax_definition : identifier -> identifier list * constr_expr ->
 
 val declare_one_assumption : coercion_flag -> assumption_kind -> Term.types ->
   Impargs.manual_explicitation list ->
-  bool (* implicit *) -> bool (* keep *) -> bool (* inline *) -> Names.variable located  -> unit
+  bool (* implicit *) -> identifier list (* keep *) -> bool (* inline *) -> Names.variable located  -> unit
   
 val set_declare_assumption_hook : (types -> unit) -> unit
 
 val declare_assumption : identifier located list ->
   coercion_flag -> assumption_kind -> local_binder list -> constr_expr -> 
-  bool -> bool -> bool -> unit
+  bool -> identifier list -> bool -> unit
 
 val declare_interning_data : 'a * Constrintern.implicits_env ->
     string * Topconstr.constr_expr * Topconstr.scope_name option -> unit
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index f733a3d5..0cda7c71 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: himsg.ml 11784 2009-01-14 11:36:32Z herbelin $ *)
+(* $Id: himsg.ml 11986 2009-03-17 11:44:20Z herbelin $ *)
 
 open Pp
 open Util
@@ -814,8 +814,8 @@ let explain_ltac_call_trace (last,trace,loc) =
       (if unboundvars <> [] or vars <> [] then
 	strbrk " (with " ++ prlist_with_sep pr_coma (fun (id,c) -> 
 	pr_id id ++ str ":=" ++ Printer.pr_lconstr c)
-	  (List.rev vars @ unboundvars)
-       else mt()) ++ str ")" in
+	  (List.rev vars @ unboundvars) ++ str ")"
+       else mt()) in
   if calls <> [] then
     let kind_of_last_call = match list_last calls with
     | Proof_type.LtacConstrInterp _ -> ", last term evaluation failed."
diff --git a/toplevel/record.ml b/toplevel/record.ml
index 4a2ef7db..4c0e34cd 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: record.ml 11809 2009-01-20 11:39:55Z aspiwack $ *)
+(* $Id: record.ml 12080 2009-04-11 16:56:20Z herbelin $ *)
 
 open Pp
 open Util
@@ -366,7 +366,7 @@ let definition_structure (kind,finite,(is_coe,(loc,idstruc)),ps,cfs,idbuild,s) =
   (* Now, younger decl in params and fields is on top *)
   let sc = Option.map mkSort s in
   let implpars, params, implfs, fields = 
-    States.with_heavy_rollback (fun () ->
+    States.with_state_protection (fun () ->
       typecheck_params_and_fields idstruc sc ps notations fs) ()
   in
     match kind with
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index c95c89d3..6a0acb52 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: vernacentries.ml 11809 2009-01-20 11:39:55Z aspiwack $ i*)
+(*i $Id: vernacentries.ml 12187 2009-06-13 19:36:59Z msozeau $ i*)
 
 (* Concrete syntax of the mathematical vernacular MV V2.6 *)
 
@@ -373,7 +373,7 @@ let vernac_assumption kind l nl=
 	List.iter (fun lid -> 
 	  if global then Dumpglob.dump_definition lid false "ax" 
 	  else Dumpglob.dump_definition lid true "var") idl;
-      declare_assumption idl is_coe kind [] c false false nl) l
+      declare_assumption idl is_coe kind [] c false [] nl) l
 
 let vernac_record k finite struc binders sort nameopt cfs =
   let const = match nameopt with 
@@ -810,14 +810,6 @@ let _ =
 let _ =
   declare_bool_option 
     { optsync  = true;
-      optname  = "manual implicit arguments";
-      optkey   = (TertiaryTable ("Manual","Implicit","Arguments"));
-      optread  = Impargs.is_manual_implicit_args;
-      optwrite = Impargs.make_manual_implicit_args }
-
-let _ =
-  declare_bool_option 
-    { optsync  = true;
       optname  = "strict implicit arguments";
       optkey   = (SecondaryTable ("Strict","Implicit"));
       optread  = Impargs.is_strict_implicit_args;
@@ -1110,9 +1102,10 @@ let vernac_print = function
   | PrintAbout qid -> msgnl (print_about qid)
   | PrintImplicit qid -> msg (print_impargs qid)
 (*spiwack: prints all the axioms and section variables used by a term *)
-  | PrintAssumptions r ->
+  | PrintAssumptions (o,r) ->
       let cstr = constr_of_global (global_with_alias r) in
-      let nassumptions = Environ.assumptions cstr (Global.env ()) in
+      let nassumptions = Environ.assumptions (Conv_oracle.get_transp_state ())
+	~add_opaque:o cstr (Global.env ()) in
       msg (Printer.pr_assumptionset (Global.env ()) nassumptions)
 
 let global_module r =
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index 3e9dfb25..4da16ea7 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: vernacexpr.ml 11809 2009-01-20 11:39:55Z aspiwack $ i*)
+(*i $Id: vernacexpr.ml 12187 2009-06-13 19:36:59Z msozeau $ i*)
 
 open Util
 open Names
@@ -65,7 +65,7 @@ type printable =
   | PrintVisibility of string option
   | PrintAbout of reference
   | PrintImplicit of reference
-  | PrintAssumptions of reference
+  | PrintAssumptions of bool * reference
 
 type search_about_item =
   | SearchSubPattern of constr_pattern_expr