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

12 files changed, 100 insertions, 204 deletions

diff --git a/contrib/interface/depends.ml b/contrib/interface/depends.ml
index e59de34a..e0f43193 100644
--- a/contrib/interface/depends.ml
+++ b/contrib/interface/depends.ml
@@ -58,8 +58,8 @@ let explore_tree pfs =
     | Refine c -> "Refine " ^ (string_of_ppcmds (Printer.prterm c))
     | Intro identifier -> "Intro"
     | Cut (bool, _, identifier, types) -> "Cut"
-    | FixRule (identifier, int, l) -> "FixRule"
-    | Cofix (identifier, l) -> "Cofix"
+    | FixRule (identifier, int, l, _) -> "FixRule"
+    | Cofix (identifier, l, _) -> "Cofix"
     | Convert_concl (types, cast_kind) -> "Convert_concl"
     | Convert_hyp named_declaration -> "Convert_hyp"
     | Thin identifier_list -> "Thin"
@@ -411,8 +411,8 @@ and depends_of_prim_rule pr acc = match pr with
   | Refine c                     -> depends_of_constr c acc
   | Intro id                     -> acc
   | Cut (_, _, _, t)             -> depends_of_constr t acc (* TODO: check what 3nd argument contains *)
-  | FixRule (_, _, l)            -> list_union_map (o depends_of_constr trd_of_3) l acc (* TODO: check what the arguments contain *)
-  | Cofix (_, l)                 -> list_union_map (o depends_of_constr snd) l acc (* TODO: check what the arguments contain *)
+  | FixRule (_, _, l, _)         -> list_union_map (o depends_of_constr trd_of_3) l acc (* TODO: check what the arguments contain *)
+  | Cofix (_, l, _)              -> list_union_map (o depends_of_constr snd) l acc (* TODO: check what the arguments contain *)
   | Convert_concl (t, _)         -> depends_of_constr t acc
   | Convert_hyp (_, None, t)     -> depends_of_constr t acc
   | Convert_hyp (_, (Some c), t) -> depends_of_constr c (depends_of_constr t acc)
diff --git a/contrib/subtac/subtac.ml b/contrib/subtac/subtac.ml
index ba00fce5..c0b64379 100644
--- a/contrib/subtac/subtac.ml
+++ b/contrib/subtac/subtac.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: subtac.ml 11800 2009-01-18 18:34:15Z msozeau $ *)
+(* $Id: subtac.ml 12194 2009-06-17 16:38:09Z msozeau $ *)
 
 open Global
 open Pp
@@ -99,7 +99,7 @@ let declare_assumption env isevars idl is_coe k bl c nl =
       Subtac_pretyping.subtac_process env isevars id [] (Command.generalize_constr_expr c bl) None 
     in
     let c = solve_tccs_in_type env id isevars evm c typ in
-      List.iter (Command.declare_one_assumption is_coe k c imps false false nl) idl
+      List.iter (Command.declare_one_assumption is_coe k c imps false [] nl) idl
   else
     errorlabstrm "Command.Assumption"
 	(str "Cannot declare an assumption while in proof editing mode.")
@@ -127,7 +127,6 @@ let check_fresh (loc,id) =
 let subtac (loc, command) =
   check_required_library ["Coq";"Init";"Datatypes"];
   check_required_library ["Coq";"Init";"Specif"];
-  check_required_library ["Coq";"Program";"Tactics"];
   let env = Global.env () in
   let isevars = ref (create_evar_defs Evd.empty) in
   try
@@ -143,7 +142,7 @@ let subtac (loc, command) =
 	  start_proof_and_print env isevars (Some lid) (Global, DefinitionBody Definition) (bl,t) 
 	    (fun _ _ -> ())
       | DefineBody (bl, _, c, tycon) -> 
-	  ignore(Subtac_pretyping.subtac_proof defkind env isevars id bl c tycon))
+	  ignore(Subtac_pretyping.subtac_proof defkind hook env isevars id bl c tycon))
   | VernacFixpoint (l, b) -> 
       List.iter (fun ((lid, _, _, _, _), _) -> 
 	check_fresh lid;
@@ -237,9 +236,6 @@ let subtac (loc, command) =
 	  debug 2 (Himsg.explain_pretype_error env exn);
 	  raise e
 
-      | e'' -> msg_warning (str "Unexpected exception: " ++ Cerrors.explain_exn e'');
-	  raise e)
+      | e'' -> raise e)
 	
-  | e -> 
-      msg_warning (str "Uncatched exception: " ++ Cerrors.explain_exn e);
-      raise e
+  | e -> raise e
diff --git a/contrib/subtac/subtac_cases.ml b/contrib/subtac/subtac_cases.ml
index 1d213db9..bd06407f 100644
--- a/contrib/subtac/subtac_cases.ml
+++ b/contrib/subtac/subtac_cases.ml
@@ -7,7 +7,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: subtac_cases.ml 11897 2009-02-09 19:28:02Z barras $ *)
+(* $Id: subtac_cases.ml 12194 2009-06-17 16:38:09Z msozeau $ *)
 
 open Cases
 open Util
@@ -301,8 +301,8 @@ module Cases_F(Coercion : Coercion.S) : S = struct
 
 let inh_coerce_to_ind isevars env ty tyi =
   let expected_typ = inductive_template isevars env None tyi in
-     (* devrait être indifférent d'exiger leq ou pas puisque pour 
-        un inductif cela doit être égal *)
+     (* devrait être indifférent d'exiger leq ou pas puisque pour 
+        un inductif cela doit être égal *)
   let _ = e_cumul env isevars expected_typ ty in ()
 
 let unify_tomatch_with_patterns isevars env loc typ pats =
@@ -696,9 +696,9 @@ let insert_aliases_eqn sign eqnnames alias_rest eqn =
 	    
 
 let insert_aliases env sigma alias eqns =
-  (* Là, y a une faiblesse, si un alias est utilisé dans un cas par *)
-  (* défaut présent mais inutile, ce qui est le cas général, l'alias *)
-  (* est introduit même s'il n'est pas utilisé dans les cas réguliers *)
+  (* Là, y a une faiblesse, si un alias est utilisé dans un cas par *)
+  (* défaut présent mais inutile, ce qui est le cas général, l'alias *)
+  (* est introduit même s'il n'est pas utilisé dans les cas réguliers *)
   let eqnsnames = List.map (fun eqn -> List.hd eqn.alias_stack) eqns in
   let alias_rests = List.map (fun eqn -> List.tl eqn.alias_stack) eqns in
   (* names2 takes the meet of all needed aliases *)
@@ -843,7 +843,7 @@ let infer_predicate loc env isevars typs cstrs indf =
       (* Non dependent case -> turn it into a (dummy) dependent one *)
       let sign = (Anonymous,None,build_dependent_inductive env indf)::sign in
       let pred = it_mkLambda_or_LetIn (lift (List.length sign) mtyp) sign in
-      (true,pred) (* true = dependent -- par défaut *)
+      (true,pred) (* true = dependent -- par défaut *)
     else
 (*
       let s = get_sort_of env (evars_of isevars) typs.(0) in
@@ -1294,7 +1294,7 @@ and compile_alias pb (deppat,nondeppat,d,t) rest =
   List.fold_left mkSpecialLetInJudge j sign
 
 (* pour les alias des initiaux, enrichir les env de ce qu'il faut et
-substituer après par les initiaux *)
+substituer après par les initiaux *)
 
 (**************************************************************************)
 (* Preparation of the pattern-matching problem                            *)
@@ -1319,99 +1319,6 @@ let matx_of_eqns env eqns =
 (************************************************************************)
 (* preparing the elimination predicate if any                          *)
 
-let build_expected_arity env isevars isdep tomatchl =
-  let cook n = function
-    | _,IsInd (_,IndType(indf,_)) ->
-        let indf' = lift_inductive_family n indf in
-	Some (build_dependent_inductive env indf', fst (get_arity env indf'))
-    | _,NotInd _ -> None
-  in
-  let rec buildrec n env = function
-    | [] -> new_Type ()
-    | tm::ltm ->
-	match cook n tm with
-	  | None -> buildrec n env ltm
-	  | Some (ty1,aritysign) ->
-	      let rec follow n env = function
-		| d::sign ->
-		    mkProd_or_LetIn_name env
-		      (follow (n+1) (push_rel d env) sign) d
-		| [] ->
-		    if isdep then
-		      mkProd (Anonymous, ty1, 
-			      buildrec (n+1)
-				(push_rel_assum (Anonymous, ty1) env)
-				ltm)
-		    else buildrec n env ltm
-	      in follow n env (List.rev aritysign)
-  in buildrec 0 env tomatchl
-
-let extract_predicate_conclusion isdep tomatchl pred =
-  let cook = function
-    | _,IsInd (_,IndType(_,args)) -> Some (List.length args)
-    | _,NotInd _ -> None in
-  let rec decomp_lam_force n l p =
-    if n=0 then (l,p) else
-    match kind_of_term p with
-      | Lambda (na,_,c) -> decomp_lam_force (n-1) (na::l) c
-      | _ -> (* eta-expansion *)
-          let na = Name (id_of_string "x") in
-          decomp_lam_force (n-1) (na::l) (applist (lift 1 p, [mkRel 1])) in
-  let rec buildrec allnames p = function
-    | [] -> (List.rev allnames,p)
-    | tm::ltm ->
-	match cook tm with
-	  | None -> 
-              let p = 
-                (* adjust to a sign containing the NotInd's *)
-                if isdep then lift 1 p else p in
-              let names = if isdep then [Anonymous] else [] in
-              buildrec (names::allnames) p ltm
-	  | Some n ->
-              let n = if isdep then n+1 else n in
-              let names,p = decomp_lam_force n [] p in
-              buildrec (names::allnames) p ltm
-  in buildrec [] pred tomatchl
-
-let set_arity_signature dep n arsign tomatchl pred x =
-  (* avoid is not exhaustive ! *)
-  let rec decomp_lam_force n avoid l p =
-    if n = 0 then (List.rev l,p,avoid) else
-    match p with
-      | RLambda (_,(Name id as na),k,_,c) -> 
-          decomp_lam_force (n-1) (id::avoid) (na::l) c
-      | RLambda (_,(Anonymous as na),k,_,c) -> decomp_lam_force (n-1) avoid (na::l) c
-      | _ ->
-          let x = next_ident_away (id_of_string "x") avoid in
-          decomp_lam_force (n-1) (x::avoid) (Name x :: l) 
-          (* eta-expansion *)
-            (let a = RVar (dummy_loc,x) in
-             match p with
-               | RApp (loc,p,l) -> RApp (loc,p,l@[a])
-               | _ -> (RApp (dummy_loc,p,[a]))) in
-  let rec decomp_block avoid p = function
-    | ([], _) -> x := Some p
-    | ((_,IsInd (_,IndType(indf,realargs)))::l),(y::l')  ->
-	let (ind,params) = dest_ind_family indf in
-        let (nal,p,avoid') = decomp_lam_force (List.length realargs) avoid [] p 
-        in
-        let na,p,avoid' = 
-          if dep then decomp_lam_force 1 avoid' [] p else [Anonymous],p,avoid'
-        in 
-        y :=
-        (List.hd na,
-         if List.for_all ((=) Anonymous) nal then
-           None
-         else
-           Some (dummy_loc, ind, (List.map (fun _ -> Anonymous) params)@nal));
-        decomp_block avoid' p (l,l')
-    | (_::l),(y::l') ->
-        y := (Anonymous,None);
-        decomp_block avoid p (l,l')
-    | _ -> anomaly "set_arity_signature"
-  in
-  decomp_block [] pred (tomatchl,arsign)
-
 let oldprepare_predicate_from_tycon loc dep env isevars tomatchs sign c =
   let cook (n, l, env, signs) = function
     | c,IsInd (_,IndType(indf,realargs)) ->
@@ -1569,9 +1476,6 @@ let eq_id avoid id =
 
 let mk_eq typ x y = mkApp (Lazy.force eq_ind, [| typ; x ; y |])
 let mk_eq_refl typ x = mkApp (Lazy.force eq_refl, [| typ; x |])
-let mk_JMeq typ x typ' y = 
-  mkApp (Lazy.force Subtac_utils.jmeq_ind, [| typ; x ; typ'; y |])
-let mk_JMeq_refl typ x = mkApp (Lazy.force Subtac_utils.jmeq_refl, [| typ; x |])
     
 let hole = RHole (dummy_loc, Evd.QuestionMark (Evd.Define true))
 
@@ -1828,24 +1732,6 @@ let constrs_of_pats typing_fun env isevars eqns tomatchs sign neqs arity =
 
  * A type constraint but no annotation case: it is assumed non dependent.
  *)
-
-let prepare_predicate_from_rettyp loc typing_fun isevars env tomatchs sign tycon rtntyp =
-  (* We extract the signature of the arity *)
-  let arsign = extract_arity_signature env tomatchs sign in
-  let env = List.fold_right push_rels arsign env in
-  let allnames = List.rev (List.map (List.map pi1) arsign) in
-    match rtntyp with
-      | Some rtntyp ->
-	  let predcclj = typing_fun (mk_tycon (new_Type ())) env rtntyp in
-	  let predccl = (j_nf_isevar !isevars predcclj).uj_val in      
-	    Some (build_initial_predicate true allnames predccl)
-      | None -> 
-	  match valcon_of_tycon tycon with
-	    | Some ty -> 
-		let names,pred = 
-		  oldprepare_predicate_from_tycon loc false env isevars tomatchs sign ty
-		in Some (build_initial_predicate true names pred)
-	    | None -> None
   
 let lift_ctx n ctx = 
   let ctx', _ =
@@ -1862,7 +1748,7 @@ let abstract_tomatch env tomatchs =
 	     Rel n -> (lift lenctx c, lift_tomatch_type lenctx t) :: prev, ctx, names
 	   | _ -> 
 	       let name = next_ident_away_from (id_of_string "filtered_var") names in
-		 (mkRel 1, lift_tomatch_type 1 t) :: lift_ctx 1 prev, 
+		 (mkRel 1, lift_tomatch_type (succ lenctx) t) :: lift_ctx 1 prev, 
 	       (Name name, Some (lift lenctx c), lift lenctx $ type_of_tomatch t) :: ctx, 
 	       name :: names)
       ([], [], []) tomatchs
@@ -1912,7 +1798,7 @@ let build_dependent_signature env evars avoid tomatchs arsign =
 		      let previd, id = 
 			let name = 
 			  match kind_of_term arg with 
-			      Rel n -> pi1 (lookup_rel n (rel_context env))
+			      Rel n -> pi1 (Environ.lookup_rel n env)
 			    | _ -> name
 			in
 			  make_prime avoid name 
@@ -2025,6 +1911,25 @@ let prepare_predicate_from_arsign_tycon loc env evm tomatchs arsign c =
 	ignore(Typing.sort_of env' evm pred); pred
     with _ -> lift nar c
 
+
+let prepare_predicate_from_rettyp loc typing_fun isevars env tomatchs sign tycon rtntyp =
+  (* We extract the signature of the arity *)
+  let arsign = extract_arity_signature env tomatchs sign in
+  let newenv = List.fold_right push_rels arsign env in
+  let allnames = List.rev (List.map (List.map pi1) arsign) in
+    match rtntyp with
+      | Some rtntyp ->
+	  let predcclj = typing_fun (mk_tycon (new_Type ())) newenv rtntyp in
+	  let predccl = (j_nf_isevar !isevars predcclj).uj_val in      
+	    Some (build_initial_predicate true allnames predccl)
+      | None -> 
+	  match valcon_of_tycon tycon with
+	    | Some ty -> 
+		let pred = 
+		  prepare_predicate_from_arsign_tycon loc env (Evd.evars_of !isevars) tomatchs arsign ty
+		in Some (build_initial_predicate true allnames pred)
+	    | None -> None
+
 let compile_cases loc style (typing_fun, isevars) (tycon : Evarutil.type_constraint) env (predopt, tomatchl, eqns) =
 
   let typing_fun tycon env = typing_fun tycon env isevars in
@@ -2103,26 +2008,25 @@ let compile_cases loc style (typing_fun, isevars) (tycon : Evarutil.type_constra
       (* with the type of arguments to match *)
       let tmsign = List.map snd tomatchl in
       let pred = prepare_predicate_from_rettyp loc typing_fun isevars env tomatchs tmsign tycon predopt in
-	
-	  (* We push the initial terms to match and push their alias to rhs' envs *)
-	  (* names of aliases will be recovered from patterns (hence Anonymous here) *)
-	  let initial_pushed = List.map (fun tm -> Pushed (tm,[])) tomatchs in
-	    
-	  let pb =
-	    { env      = env;
-	      isevars  = isevars;
-	      pred     = pred;
-	      tomatch  = initial_pushed;
-	      history  = start_history (List.length initial_pushed);
-	      mat      = matx;
-	      caseloc  = loc;
-	      casestyle= style;
-	      typing_function = typing_fun } in
-	    
-	  let j = compile pb in
-	  (* We check for unused patterns *)
-	  List.iter (check_unused_pattern env) matx;
-	    inh_conv_coerce_to_tycon loc env isevars j tycon	  
 
+      (* We push the initial terms to match and push their alias to rhs' envs *)
+      (* names of aliases will be recovered from patterns (hence Anonymous here) *)
+      let initial_pushed = List.map (fun tm -> Pushed (tm,[])) tomatchs in
+      let pb =
+	{ env      = env;
+	  isevars  = isevars;
+	  pred     = pred;
+	  tomatch  = initial_pushed;
+	  history  = start_history (List.length initial_pushed);
+	  mat      = matx;
+	  caseloc  = loc;
+	  casestyle= style;
+	  typing_function = typing_fun } in
+	
+      let j = compile pb in
+	(* We check for unused patterns *)
+	List.iter (check_unused_pattern env) matx;
+	inh_conv_coerce_to_tycon loc env isevars j tycon	  
+	  
 end
   
diff --git a/contrib/subtac/subtac_classes.ml b/contrib/subtac/subtac_classes.ml
index 0d44a0c0..9b692d85 100644
--- a/contrib/subtac/subtac_classes.ml
+++ b/contrib/subtac/subtac_classes.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: subtac_classes.ml 11800 2009-01-18 18:34:15Z msozeau $ i*)
+(*i $Id: subtac_classes.ml 12187 2009-06-13 19:36:59Z msozeau $ i*)
 
 open Pretyping
 open Evd
@@ -182,7 +182,7 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(generalize=true) p
   in
     isevars := undefined_evars !isevars;
     Evarutil.check_evars env Evd.empty !isevars termtype;
-    let hook gr = 
+    let hook vis gr = 
       let cst = match gr with ConstRef kn -> kn | _ -> assert false in
       let inst = Typeclasses.new_instance k pri global cst in
 	Impargs.declare_manual_implicits false gr ~enriching:false imps;
diff --git a/contrib/subtac/subtac_command.ml b/contrib/subtac/subtac_command.ml
index 4876b065..c8c7ff72 100644
--- a/contrib/subtac/subtac_command.ml
+++ b/contrib/subtac/subtac_command.ml
@@ -390,7 +390,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 (Command.declare_interning_data impls) notations;
       list_map3 (interp_fix_body evdref env_rec impls) fixctxs fixl fixccls)
       () in
diff --git a/contrib/subtac/subtac_obligations.ml b/contrib/subtac/subtac_obligations.ml
index d2e831ef..3dcd43d2 100644
--- a/contrib/subtac/subtac_obligations.ml
+++ b/contrib/subtac/subtac_obligations.ml
@@ -17,8 +17,6 @@ open Evd
 open Declare
 open Proof_type
 
-type definition_hook = global_reference -> unit
-
 let ppwarn cmd = Pp.warn (str"Program:" ++ cmd)
 let pperror cmd = Util.errorlabstrm "Program" cmd
 let error s = pperror (str s)
@@ -56,14 +54,14 @@ type program_info = {
   prg_implicits : (Topconstr.explicitation * (bool * bool)) list;
   prg_notations : notations ;
   prg_kind : definition_kind;
-  prg_hook : definition_hook;
+  prg_hook : Tacexpr.declaration_hook;
 }
 
 let assumption_message id =
   Flags.if_verbose message ((string_of_id id) ^ " is assumed")
 
 let default_tactic : Proof_type.tactic ref = ref Refiner.tclIDTAC
-let default_tactic_expr : Tacexpr.glob_tactic_expr ref = ref (Obj.magic ())
+let default_tactic_expr : Tacexpr.glob_tactic_expr ref = ref (Tacexpr.TacId [])
 
 let set_default_tactic t = default_tactic_expr := t; default_tactic := Tacinterp.eval_tactic t
 
@@ -203,7 +201,7 @@ let declare_definition prg =
 	  if Impargs.is_implicit_args () || prg.prg_implicits <> [] then
 	    Impargs.declare_manual_implicits false gr prg.prg_implicits;
 	  print_message (Subtac_utils.definition_message prg.prg_name);
-	  prg.prg_hook gr;
+	  prg.prg_hook local gr;
 	  gr
 
 open Pp
@@ -234,6 +232,7 @@ let reduce_fix =
 
 let declare_mutual_definition l =
   let len = List.length l in
+  let first = List.hd l in
   let fixdefs, fixtypes, fiximps = 
     list_split3
       (List.map (fun x -> 
@@ -241,11 +240,11 @@ let declare_mutual_definition l =
 	  snd (decompose_lam_n len subs), snd (decompose_prod_n len typ), x.prg_implicits) l)
   in
 (*   let fixdefs = List.map reduce_fix fixdefs in *)
-  let fixkind = Option.get (List.hd l).prg_fixkind in
+  let fixkind = Option.get first.prg_fixkind in
   let arrrec, recvec = Array.of_list fixtypes, Array.of_list fixdefs in
   let fixdecls = (Array.of_list (List.map (fun x -> Name x.prg_name) l), arrrec, recvec) in
-  let boxed = true (* TODO *) in
-  let fixnames = (List.hd l).prg_deps in
+  let (local,boxed,kind) = first.prg_kind in
+  let fixnames = first.prg_deps in
   let kind = if fixkind <> IsCoFixpoint then Fixpoint else CoFixpoint in
   let indexes, fixdecls =
     match fixkind with
@@ -260,9 +259,11 @@ let declare_mutual_definition l =
   (* Declare the recursive definitions *)
   let kns = list_map4 (declare_fix boxed kind) fixnames fixdecls fixtypes fiximps in
     (* Declare notations *)
-    List.iter (Command.declare_interning_data ([],[])) (List.hd l).prg_notations;
+    List.iter (Command.declare_interning_data ([],[])) first.prg_notations;
     Flags.if_verbose ppnl (Command.recursive_message kind indexes fixnames);
-    (match List.hd kns with ConstRef kn -> kn | _ -> assert false)
+    let gr = List.hd kns in
+    let kn = match gr with ConstRef kn -> kn | _ -> assert false in
+      first.prg_hook local gr; kn
       
 let declare_obligation obl body =
   match obl.obl_status with
@@ -525,7 +526,7 @@ let show_term n =
 	      my_print_constr (Global.env ()) prg.prg_type ++ spc () ++ str ":=" ++ fnl ()
 	    ++ my_print_constr (Global.env ()) prg.prg_body)
 
-let add_definition n b t ?(implicits=[]) ?(kind=Global,false,Definition) ?tactic ?(hook=fun x -> ()) obls =
+let add_definition n b t ?(implicits=[]) ?(kind=Global,false,Definition) ?tactic ?(hook=fun _ _ -> ()) obls =
   Flags.if_verbose pp (str (string_of_id n) ++ str " has type-checked");
   let prg = init_prog_info n b t [] None [] obls implicits kind hook in
   let obls,_ = prg.prg_obligations in
@@ -543,11 +544,11 @@ let add_definition n b t ?(implicits=[]) ?(kind=Global,false,Definition) ?tactic
 	| Remain rem -> Flags.if_verbose (fun () -> show_obligations ~msg:false (Some n)) (); res
 	| _ -> res)
 	
-let add_mutual_definitions l ?tactic ?(kind=Global,false,Definition) notations fixkind =
+let add_mutual_definitions l ?tactic ?(kind=Global,false,Definition) ?(hook=fun _ _ -> ()) notations fixkind =
   let deps = List.map (fun (n, b, t, imps, obls) -> n) l in
   let upd = List.fold_left
       (fun acc (n, b, t, imps, obls) ->
-	let prg = init_prog_info n b t deps (Some fixkind) notations obls imps kind (fun x -> ()) in
+	let prg = init_prog_info n b t deps (Some fixkind) notations obls imps kind hook in
 	  ProgMap.add n prg acc)
       !from_prg l
   in
diff --git a/contrib/subtac/subtac_obligations.mli b/contrib/subtac/subtac_obligations.mli
index 60c0a413..766af2fa 100644
--- a/contrib/subtac/subtac_obligations.mli
+++ b/contrib/subtac/subtac_obligations.mli
@@ -21,13 +21,11 @@ val default_tactic : unit -> Proof_type.tactic
 val set_proofs_transparency : bool -> unit (* true = All transparent, false = Opaque if possible *)
 val get_proofs_transparency : unit -> bool
 
-type definition_hook = global_reference -> unit
-
 val add_definition : Names.identifier ->  Term.constr -> Term.types -> 
   ?implicits:(Topconstr.explicitation * (bool * bool)) list ->
   ?kind:Decl_kinds.definition_kind ->
   ?tactic:Proof_type.tactic ->
-  ?hook:definition_hook -> obligation_info -> progress
+  ?hook:Tacexpr.declaration_hook -> obligation_info -> progress
 
 type notations = (string * Topconstr.constr_expr * Topconstr.scope_name option) list
 
@@ -36,6 +34,7 @@ val add_mutual_definitions :
       (Topconstr.explicitation * (bool * bool)) list * obligation_info) list -> 
   ?tactic:Proof_type.tactic ->
   ?kind:Decl_kinds.definition_kind ->
+  ?hook:Tacexpr.declaration_hook -> 
   notations ->
   Command.fixpoint_kind -> unit
 
diff --git a/contrib/subtac/subtac_pretyping.ml b/contrib/subtac/subtac_pretyping.ml
index 07a75720..3ae7c95d 100644
--- a/contrib/subtac/subtac_pretyping.ml
+++ b/contrib/subtac/subtac_pretyping.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: subtac_pretyping.ml 11574 2008-11-10 13:45:05Z msozeau $ *)
+(* $Id: subtac_pretyping.ml 12187 2009-06-13 19:36:59Z msozeau $ *)
 
 open Global
 open Pp
@@ -84,13 +84,6 @@ let find_with_index x l =
     | [] -> raise Not_found
   in aux 0 l
 
-let list_split_at index l = 
-  let rec aux i acc = function
-      hd :: tl when i = index -> (List.rev acc), tl
-    | hd :: tl -> aux (succ i) (hd :: acc) tl
-    | [] -> failwith "list_split_at: Invalid argument"
-  in aux 0 [] l
-
 open Vernacexpr
 
 let coqintern_constr evd env : Topconstr.constr_expr -> Rawterm.rawconstr = Constrintern.intern_constr (evars_of evd) env
@@ -136,9 +129,9 @@ let subtac_process env isevars id bl c tycon =
 
 open Subtac_obligations
 
-let subtac_proof kind env isevars id bl c tycon =
+let subtac_proof kind hook env isevars id bl c tycon =
   let evm, coqc, coqt, imps = subtac_process env isevars id bl c tycon in
   let evm' = Subtac_utils.evars_of_term evm Evd.empty coqc in
   let evm' = Subtac_utils.evars_of_term evm evm' coqt in
   let evars, def, ty = Eterm.eterm_obligations env id !isevars evm' 0 coqc coqt in
-    add_definition id def ty ~implicits:imps ~kind:kind evars
+    add_definition id def ty ~implicits:imps ~kind ~hook evars
diff --git a/contrib/subtac/subtac_pretyping.mli b/contrib/subtac/subtac_pretyping.mli
index 1d8eb250..ba0b7cd2 100644
--- a/contrib/subtac/subtac_pretyping.mli
+++ b/contrib/subtac/subtac_pretyping.mli
@@ -19,5 +19,6 @@ val interp :
 val subtac_process : env -> evar_defs ref -> identifier -> local_binder list ->
   constr_expr -> constr_expr option -> evar_map * constr * types * manual_explicitation list
 
-val subtac_proof : Decl_kinds.definition_kind -> env -> evar_defs ref -> identifier -> local_binder list ->
+val subtac_proof : Decl_kinds.definition_kind -> Tacexpr.declaration_hook -> 
+  env -> evar_defs ref -> identifier -> local_binder list ->
   constr_expr -> constr_expr option -> Subtac_obligations.progress
diff --git a/contrib/subtac/subtac_utils.ml b/contrib/subtac/subtac_utils.ml
index cdbc4023..2ee2018e 100644
--- a/contrib/subtac/subtac_utils.ml
+++ b/contrib/subtac/subtac_utils.ml
@@ -64,15 +64,17 @@ let eqdep_rec = lazy (init_constant ["Logic";"Eqdep"] "eq_dep_rec")
 let eqdep_ind_ref = lazy (init_reference [ "Logic";"Eqdep"] "eq_dep")
 let eqdep_intro_ref = lazy (init_reference [ "Logic";"Eqdep"] "eq_dep_intro")
 
-let jmeq_ind =   
-  lazy (check_required_library ["Coq";"Logic";"JMeq"]; 
-	init_constant ["Logic";"JMeq"] "JMeq")
-let jmeq_rec = 
-  lazy (check_required_library ["Coq";"Logic";"JMeq"]; 
-	init_constant ["Logic";"JMeq"] "JMeq_rec")
-let jmeq_refl = 
-  lazy (check_required_library ["Coq";"Logic";"JMeq"];
-	init_constant ["Logic";"JMeq"] "JMeq_refl")
+let jmeq_ind () =   
+  check_required_library ["Coq";"Logic";"JMeq"]; 
+  init_constant ["Logic";"JMeq"] "JMeq"
+
+let jmeq_rec () = 
+  check_required_library ["Coq";"Logic";"JMeq"]; 
+  init_constant ["Logic";"JMeq"] "JMeq_rec"
+
+let jmeq_refl () = 
+  check_required_library ["Coq";"Logic";"JMeq"];
+  init_constant ["Logic";"JMeq"] "JMeq_refl"
 
 let ex_ind = lazy (init_constant ["Init"; "Logic"] "ex")
 let ex_intro = lazy (init_reference ["Init"; "Logic"] "ex_intro")
@@ -277,8 +279,8 @@ let mkSubset name typ prop =
 
 let mk_eq typ x y = mkApp (Lazy.force eq_ind, [| typ; x ; y |])
 let mk_eq_refl typ x = mkApp (Lazy.force eq_refl, [| typ; x |])
-let mk_JMeq typ x typ' y = mkApp (Lazy.force jmeq_ind, [| typ; x ; typ'; y |])
-let mk_JMeq_refl typ x = mkApp (Lazy.force jmeq_refl, [| typ; x |])
+let mk_JMeq typ x typ' y = mkApp (jmeq_ind (), [| typ; x ; typ'; y |])
+let mk_JMeq_refl typ x = mkApp (jmeq_refl (), [| typ; x |])
 
 let unsafe_fold_right f = function
     hd :: tl -> List.fold_right f tl hd
diff --git a/contrib/subtac/subtac_utils.mli b/contrib/subtac/subtac_utils.mli
index 964f668f..9c014286 100644
--- a/contrib/subtac/subtac_utils.mli
+++ b/contrib/subtac/subtac_utils.mli
@@ -45,9 +45,9 @@ val and_typ : constr lazy_t
 val eqdep_ind : constr lazy_t
 val eqdep_rec : constr lazy_t
 
-val jmeq_ind : constr lazy_t
-val jmeq_rec : constr lazy_t
-val jmeq_refl : constr lazy_t
+val jmeq_ind : unit -> constr
+val jmeq_rec : unit -> constr
+val jmeq_refl : unit -> constr
 
 val boolind : constr lazy_t
 val sumboolind : constr lazy_t
@@ -103,7 +103,7 @@ val mk_ex_pi1 : constr -> constr -> constr -> constr
 val mk_ex_pi1 : constr -> constr -> constr -> constr
 val mk_eq : types -> constr -> constr -> types
 val mk_eq_refl : types -> constr -> constr
-val mk_JMeq : types -> constr-> types -> constr -> types
+val mk_JMeq : types -> constr -> types -> constr -> types
 val mk_JMeq_refl : types -> constr -> constr
 val mk_conj : types list -> types
 val mk_not : types -> types
diff --git a/contrib/xml/proofTree2Xml.ml4 b/contrib/xml/proofTree2Xml.ml4
index a501fb6a..7503d632 100644
--- a/contrib/xml/proofTree2Xml.ml4
+++ b/contrib/xml/proofTree2Xml.ml4
@@ -82,8 +82,8 @@ let first_word s =
 let string_of_prim_rule x = match x with
   | Proof_type.Intro _-> "Intro"
   | Proof_type.Cut _ -> "Cut"
-  | Proof_type.FixRule (_,_,_) -> "FixRule"
-  | Proof_type.Cofix (_,_)-> "Cofix"
+  | Proof_type.FixRule _ -> "FixRule"
+  | Proof_type.Cofix _ -> "Cofix"
   | Proof_type.Refine _ -> "Refine"
   | Proof_type.Convert_concl _ -> "Convert_concl"
   | Proof_type.Convert_hyp _->"Convert_hyp"