Merge commit 'upstream/8.1.gamma' into 8.1

18 files changed, 582 insertions, 165 deletions

diff --git a/proofs/decl_expr.mli b/proofs/decl_expr.mli
new file mode 100644
index 00000000..24af3842
--- /dev/null
+++ b/proofs/decl_expr.mli
@@ -0,0 +1,108 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* $Id:$ *)
+
+open Names
+open Util
+open Tacexpr
+
+type ('constr,'tac) justification =
+  By_tactic of 'tac
+| Automated of 'constr list
+
+type 'it statement = 
+    {st_label:name;
+     st_it:'it}
+
+type thesis_kind =
+    Plain
+  | Sub of int
+  | For of identifier
+
+type 'this or_thesis =
+    This of 'this
+  | Thesis of thesis_kind
+
+type side = Lhs | Rhs
+
+type elim_type =
+    ET_Case_analysis
+  | ET_Induction
+
+type block_type =
+    B_proof
+  | B_claim
+  | B_focus
+  | B_elim of elim_type
+
+type ('it,'constr,'tac) cut =
+    {cut_stat: 'it statement;
+     cut_by: ('constr,'tac) justification}
+
+type ('var,'constr) hyp = 
+    Hvar of 'var 
+  | Hprop of 'constr statement
+
+type ('constr,'tac) casee = 
+    Real of 'constr 
+  | Virtual of ('constr,'constr,'tac) cut
+
+type ('hyp,'constr,'pat,'tac) bare_proof_instr =
+  | Pthen of ('hyp,'constr,'pat,'tac) bare_proof_instr
+  | Pthus of ('hyp,'constr,'pat,'tac) bare_proof_instr
+  | Phence of ('hyp,'constr,'pat,'tac) bare_proof_instr
+  | Pcut of ('constr or_thesis,'constr,'tac) cut
+  | Prew of side * ('constr,'constr,'tac) cut
+  | Passume of ('hyp,'constr) hyp list
+  | Plet of ('hyp,'constr) hyp list
+  | Pgiven of ('hyp,'constr) hyp list
+  | Pconsider of 'constr*('hyp,'constr) hyp list
+  | Pclaim of 'constr statement
+  | Pfocus of 'constr statement
+  | Pdefine of identifier * 'hyp list * 'constr
+  | Pcast of identifier or_thesis * 'constr
+  | Psuppose of ('hyp,'constr) hyp list 
+  | Pcase of 'hyp list*'pat*(('hyp,'constr or_thesis) hyp list) 
+  | Ptake of 'constr list 
+  | Pper of elim_type * ('constr,'tac) casee
+  | Pend of block_type
+  | Pescape
+
+type emphasis = int
+
+type ('hyp,'constr,'pat,'tac) gen_proof_instr=
+    {emph: emphasis;
+     instr: ('hyp,'constr,'pat,'tac) bare_proof_instr }
+
+
+type raw_proof_instr =
+    ((identifier*(Topconstr.constr_expr option)) located,
+     Topconstr.constr_expr,
+     Topconstr.cases_pattern_expr,
+     raw_tactic_expr) gen_proof_instr
+
+type glob_proof_instr =
+    ((identifier*(Genarg.rawconstr_and_expr option)) located,
+     Genarg.rawconstr_and_expr,  
+     Topconstr.cases_pattern_expr,
+     Tacexpr.glob_tactic_expr) gen_proof_instr
+
+type proof_pattern = 
+    {pat_vars: Term.types statement list;
+     pat_aliases: (Term.constr*Term.types) statement list;
+     pat_constr: Term.constr;
+     pat_typ: Term.types;
+     pat_pat: Rawterm.cases_pattern;
+     pat_expr: Topconstr.cases_pattern_expr}
+
+type proof_instr =
+    (Term.constr statement,
+     Term.constr, 
+     proof_pattern,
+     Tacexpr.glob_tactic_expr) gen_proof_instr
diff --git a/proofs/decl_mode.ml b/proofs/decl_mode.ml
new file mode 100644
index 00000000..094c5625
--- /dev/null
+++ b/proofs/decl_mode.ml
@@ -0,0 +1,121 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* $Id:$ *)
+
+open Names
+open Term
+open Evd
+open Util
+
+let daimon_flag = ref false
+
+let set_daimon_flag () = daimon_flag:=true 
+let clear_daimon_flag () = daimon_flag:=false
+let get_daimon_flag () = !daimon_flag 
+
+type command_mode =
+    Mode_tactic
+  | Mode_proof
+  | Mode_none
+
+let mode_of_pftreestate pts =
+  let goal = sig_it (Refiner.top_goal_of_pftreestate pts) in
+    if goal.evar_extra = None then
+      Mode_tactic 
+    else
+      Mode_proof
+	  
+let get_current_mode () =
+  try 
+    mode_of_pftreestate (Pfedit.get_pftreestate ())
+  with _ -> Mode_none
+
+let check_not_proof_mode str =
+ if get_current_mode () = Mode_proof then
+   error str
+
+type split_tree=
+    Push of (Idset.t * split_tree)
+  | Split of (Idset.t * inductive * (Idset.t * split_tree) option array)
+  | Pop of split_tree
+  | End_of_branch of (identifier * int)
+
+type elim_kind =
+    EK_dep of split_tree
+  | EK_nodep
+  | EK_unknown
+
+type per_info = 
+    {per_casee:constr;
+     per_ctype:types;
+     per_ind:inductive;
+     per_pred:constr;
+     per_args:constr list;
+     per_params:constr list;
+     per_nparams:int}
+
+type stack_info = 
+    Per of Decl_expr.elim_type * per_info * elim_kind * identifier list
+  | Suppose_case
+  | Claim
+  | Focus_claim
+
+type pm_info =
+    { pm_last: Names.name (* anonymous if none *);
+      pm_hyps: Idset.t;
+      pm_partial_goal : constr ; (* partial goal construction *)
+      pm_subgoals : (metavariable*constr) list;
+      pm_stack : stack_info list }
+
+let pm_in,pm_out = Dyn.create "pm_info" 
+
+let get_info gl=
+  match gl.evar_extra with
+      None ->  invalid_arg "get_info"
+    | Some extra ->
+	try pm_out extra with _ -> invalid_arg "get_info"
+
+let get_stack pts = 
+  let info = get_info (sig_it (Refiner.nth_goal_of_pftreestate 1 pts)) in
+    info.pm_stack
+
+let get_top_stack pts = 
+  let info = get_info (sig_it (Refiner.top_goal_of_pftreestate pts)) in
+    info.pm_stack
+
+let get_end_command pts =
+  match mode_of_pftreestate pts with 
+      Mode_proof ->
+	Some 
+	  begin
+	    match get_top_stack pts with
+		[] -> "\"end proof\""
+	      | Claim::_ -> "\"end claim\""
+	      | Focus_claim::_-> "\"end focus\""
+	      | (Suppose_case :: Per (et,_,_,_) :: _ 
+		| Per (et,_,_,_) :: _ ) -> 
+		  begin
+		    match et with
+			Decl_expr.ET_Case_analysis -> 
+			  "\"end cases\" or start a new case"
+		      | Decl_expr.ET_Induction -> 
+			  "\"end induction\" or start a new case"
+		  end
+	      | _ -> anomaly "lonely suppose"
+	  end
+    | Mode_tactic ->
+	begin
+	  try
+	    ignore 
+	      (Refiner.up_until_matching_rule Proof_trees.is_proof_instr pts);
+	    Some "\"return\""
+	  with Not_found -> None
+	end
+    | Mode_none ->
+        error "no proof in progress"
diff --git a/proofs/decl_mode.mli b/proofs/decl_mode.mli
new file mode 100644
index 00000000..0dd1cb33
--- /dev/null
+++ b/proofs/decl_mode.mli
@@ -0,0 +1,73 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* $Id:$ *)
+
+open Names
+open Term
+open Evd
+open Tacmach
+
+val set_daimon_flag : unit -> unit
+val clear_daimon_flag : unit -> unit
+val get_daimon_flag : unit -> bool
+
+type command_mode =
+    Mode_tactic
+  | Mode_proof
+  | Mode_none
+
+val mode_of_pftreestate : pftreestate -> command_mode
+    
+val get_current_mode : unit -> command_mode
+
+val check_not_proof_mode : string -> unit
+
+type split_tree=
+    Push of  (Idset.t * split_tree)
+  | Split of (Idset.t * inductive * (Idset.t*split_tree) option array)
+  | Pop of split_tree
+  | End_of_branch of (identifier * int)
+
+type elim_kind =
+    EK_dep of split_tree
+  | EK_nodep
+  | EK_unknown
+
+
+type per_info = 
+    {per_casee:constr;
+     per_ctype:types;
+     per_ind:inductive;
+     per_pred:constr;
+     per_args:constr list;
+     per_params:constr list;
+     per_nparams:int}
+
+type stack_info = 
+    Per of Decl_expr.elim_type * per_info * elim_kind * Names.identifier list
+  | Suppose_case
+  | Claim
+  | Focus_claim
+
+type pm_info =
+    { pm_last: Names.name (* anonymous if none *);
+      pm_hyps: Idset.t;
+      pm_partial_goal : constr ; (* partial goal construction *)
+      pm_subgoals : (metavariable*constr) list;
+      pm_stack : stack_info list }
+
+val pm_in : pm_info -> Dyn.t
+
+val get_info : Proof_type.goal -> pm_info
+
+val get_end_command : pftreestate -> string option
+
+val get_stack : pftreestate -> stack_info list
+
+val get_top_stack : pftreestate -> stack_info list
diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml
index 7a23d052..79f01ba1 100644
--- a/proofs/evar_refiner.ml
+++ b/proofs/evar_refiner.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: evar_refiner.ml 8759 2006-04-28 12:24:14Z herbelin $ *)
+(* $Id: evar_refiner.ml 9154 2006-09-20 17:18:18Z corbinea $ *)
 
 open Util
 open Names
@@ -22,7 +22,7 @@ open Refiner
 
 (* w_tactic pour instantiate *) 
 
-let w_refine env ev rawc evd =
+let w_refine ev rawc evd =
   if Evd.is_defined (evars_of evd) ev then 
     error "Instantiate called on already-defined evar";
   let e_info = Evd.find (evars_of evd) ev in
@@ -45,5 +45,5 @@ let instantiate_pf_com n com pfts =
   let env = Evd.evar_env evi in
   let rawc = Constrintern.intern_constr sigma env com in 
   let evd = create_evar_defs sigma in
-  let evd' = w_refine env sp rawc evd in
+  let evd' = w_refine sp rawc evd in
   change_constraints_pftreestate (evars_of evd') pfts
diff --git a/proofs/evar_refiner.mli b/proofs/evar_refiner.mli
index 9880f2f0..baa6b19a 100644
--- a/proofs/evar_refiner.mli
+++ b/proofs/evar_refiner.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: evar_refiner.mli 6616 2005-01-21 17:18:23Z herbelin $ i*)
+(*i $Id: evar_refiner.mli 9154 2006-09-20 17:18:18Z corbinea $ i*)
 
 (*i*)
 open Names
@@ -18,7 +18,7 @@ open Refiner
 
 (* Refinement of existential variables. *)
 
-val w_refine :  env -> evar -> Rawterm.rawconstr  -> evar_defs -> evar_defs
+val w_refine : evar -> Rawterm.rawconstr  -> evar_defs -> evar_defs
 
 val instantiate_pf_com :
   int -> Topconstr.constr_expr -> pftreestate -> pftreestate
diff --git a/proofs/logic.ml b/proofs/logic.ml
index ffbc0d56..e40d1232 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: logic.ml 8871 2006-05-28 16:46:48Z herbelin $ *)
+(* $Id: logic.ml 9323 2006-10-30 23:05:29Z herbelin $ *)
 
 open Pp
 open Util
@@ -80,15 +80,15 @@ let clear_hyps ids gl =
               error (string_of_id id'^
 		        " is used in hypothesis "^string_of_id id))
 	  (global_vars_set_of_decl env d) in
-    clear_hyps ids fcheck gl.evar_hyps in
+      clear_hyps ids fcheck gl.evar_hyps in
   let ncl = gl.evar_concl in
-  if !check && cleared_ids<>[] then
-    Idset.iter
-      (fun id' ->
-        if List.mem id' cleared_ids then
-          error (string_of_id id'^" is used in conclusion"))
-      (global_vars_set env ncl);
-  mk_goal nhyps ncl
+    if !check && cleared_ids<>[] then
+      Idset.iter
+	(fun id' ->
+          if List.mem id' cleared_ids then
+            error (string_of_id id'^" is used in conclusion"))
+	(global_vars_set_drop_evar env ncl);
+    mk_goal nhyps ncl gl.evar_extra
 
 (* The ClearBody tactic *)
 
@@ -155,7 +155,7 @@ let split_sign hfrom hto l =
       	else 
 	  splitrec (d::left) (toleft or (hyp = hto)) right
   in 
-  splitrec [] false l
+    splitrec [] false l
 
 let move_after with_dep toleft (left,(idfrom,_,_ as declfrom),right) hto =
   let env = Global.env() in
@@ -214,19 +214,25 @@ let check_forward_dependencies id tail =
 		^ (string_of_id id')))
     tail
 
+let check_goal_dependency id cl =
+  let env = Global.env() in
+    if Idset.mem id (global_vars_set_drop_evar env cl) then
+      error (string_of_id id^" is used in conclusion")
 
 let rename_hyp id1 id2 sign =
   apply_to_hyp_and_dependent_on sign id1
     (fun (_,b,t) _ -> (id2,b,t))
     (fun d _ -> map_named_declaration (replace_vars [id1,mkVar id2]) d)
 
-let replace_hyp sign id d =
+let replace_hyp sign id d cl =
+  if !check then
+    check_goal_dependency id cl;
   apply_to_hyp sign id
     (fun sign _ tail ->
-       if !check then
-	 (check_backward_dependencies sign d;
-	  check_forward_dependencies id tail);
-       d)
+      if !check then
+	(check_backward_dependencies sign d;
+	 check_forward_dependencies id tail); 
+      d)
 
 (* why we dont check that id does not appear in tail ??? *)
 let insert_after_hyp sign id d =
@@ -264,6 +270,7 @@ let goal_type_of env sigma c =
 let rec mk_refgoals sigma goal goalacc conclty trm =
   let env = evar_env goal in
   let hyps = goal.evar_hyps in
+  let mk_goal hyps concl = mk_goal hyps concl goal.evar_extra in
 (*
    if  not (occur_meta trm) then
     let t'ty = (unsafe_machine env sigma trm).uj_type in 	
@@ -284,9 +291,14 @@ let rec mk_refgoals sigma goal goalacc conclty trm =
 
     | App (f,l) ->
 	let (acc',hdty) =
-	  if isInd f & not (array_exists occur_meta l) (* we could be finer *)
-	  then (goalacc,type_of_inductive_knowing_parameters env sigma (destInd f) l)
-	  else mk_hdgoals sigma goal goalacc f
+	  match kind_of_term f with
+	    | (Ind _ (* needed if defs in Type are polymorphic: | Const _*))
+		when not (array_exists occur_meta l) (* we could be finer *) ->
+		(* Sort-polymorphism of definition and inductive types *)
+		goalacc, 
+		type_of_global_reference_knowing_parameters env sigma f l
+	    | _ -> 
+		mk_hdgoals sigma goal goalacc f
 	in
 	let (acc'',conclty') =
 	  mk_arggoals sigma goal acc' hdty (Array.to_list l) in
@@ -315,6 +327,7 @@ let rec mk_refgoals sigma goal goalacc conclty trm =
 and mk_hdgoals sigma goal goalacc trm =
   let env = evar_env goal in
   let hyps = goal.evar_hyps in
+  let mk_goal hyps concl = mk_goal hyps concl goal.evar_extra in
   match kind_of_term trm with
     | Cast (c,_, ty) when isMeta c ->
 	check_typability env sigma ty;
@@ -326,8 +339,10 @@ and mk_hdgoals sigma goal goalacc trm =
 
     | App (f,l) ->
 	let (acc',hdty) = 
-	  if isInd f & not (array_exists occur_meta l) (* we could be finer *)
-	  then (goalacc,type_of_inductive_knowing_parameters env sigma (destInd f) l)
+	  if isInd f or isConst f 
+	     & not (array_exists occur_meta l) (* we could be finer *)
+	  then
+	    (goalacc,type_of_global_reference_knowing_parameters env sigma f l)
 	  else mk_hdgoals sigma goal goalacc f
 	in
 	mk_arggoals sigma goal acc' hdty (Array.to_list l)
@@ -392,6 +407,7 @@ let prim_refiner r sigma goal =
   let env = evar_env goal in
   let sign = goal.evar_hyps in
   let cl = goal.evar_concl in
+  let mk_goal hyps concl = mk_goal hyps concl goal.evar_extra in
   match r with
     (* Logical rules *)
     | Intro id ->
@@ -416,12 +432,12 @@ let prim_refiner r sigma goal =
 	(match kind_of_term (strip_outer_cast cl) with
            | Prod (_,c1,b) ->
 	       if occur_meta c1 then error_use_instantiate();
-	       let sign' = replace_hyp sign id (id,None,c1) in
+	       let sign' = replace_hyp sign id (id,None,c1) cl in
 	       let sg = mk_goal sign' (subst1 (mkVar id) b) in
 	       [sg]
            | LetIn (_,c1,t1,b) ->
 	       if occur_meta c1 then error_use_instantiate();
-	       let sign' = replace_hyp sign id (id,Some c1,t1) in
+	       let sign' = replace_hyp sign id (id,Some c1,t1) cl in
 	       let sg = mk_goal sign' (subst1 (mkVar id) b) in
 	       [sg]
 	   | _ ->
@@ -474,7 +490,8 @@ let prim_refiner r sigma goal =
 		  let _ = find_coinductive env sigma b in ()
                 with Not_found -> 
 		  error ("All methods must construct elements " ^
-			  "in coinductive types")
+			  "in coinductiv-> goal
+e types")
 	in
 	let all = (f,cl)::others in
      	List.iter (fun (_,c) -> check_is_coind env c) all;
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index fa6f8c37..565c9547 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: pfedit.ml 6947 2005-04-20 16:18:41Z coq $ *)
+(* $Id: pfedit.ml 9154 2006-09-20 17:18:18Z corbinea $ *)
 
 open Pp
 open Util
@@ -150,6 +150,14 @@ let subtree_solved () =
   is_complete_proof (proof_of_pftreestate pts) & 
   not (is_top_pftreestate pts)
 
+let tree_solved () = 
+  let pts = get_pftreestate () in
+  is_complete_proof (proof_of_pftreestate pts)
+
+let top_tree_solved () = 
+  let pts = get_pftreestate () in
+  is_complete_proof (proof_of_pftreestate (top_of_tree pts))
+
 (*********************************************************************)
 (*                 Undo functions                                    *)
 (*********************************************************************)
@@ -243,7 +251,7 @@ let set_end_tac tac =
 (*********************************************************************)
 
 let start_proof na str sign concl hook =
-  let top_goal = mk_goal sign concl in
+  let top_goal = mk_goal sign concl None in
   let ts = { 
     top_end_tac = None;
     top_goal = top_goal;
@@ -253,7 +261,6 @@ let start_proof na str sign concl hook =
   start(na,ts);
   set_current_proof na
 
-
 let solve_nth k tac =
   let pft = get_pftreestate () in
   if not (List.mem (-1) (cursor_of_pftreestate pft)) then
@@ -309,7 +316,6 @@ let traverse_prev_unproven () = mutate prev_unproven
 
 let traverse_next_unproven () = mutate next_unproven
 
-
 (* The goal focused on *)
 let focus_n = ref 0
 let make_focus n = focus_n := n
@@ -317,5 +323,11 @@ let focus () = !focus_n
 let focused_goal () = let n = !focus_n in if n=0 then 1 else n
 
 let reset_top_of_tree () = 
-  let pts = get_pftreestate () in 
-  if not (is_top_pftreestate pts) then mutate top_of_tree
+  mutate top_of_tree
+ 
+let reset_top_of_script () = 
+  mutate (fun pts -> 
+	try
+	 up_until_matching_rule is_proof_instr pts
+	with Not_found -> top_of_tree pts)
+
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index ca379d2e..8c0c7f55 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: pfedit.mli 7639 2005-12-02 10:01:15Z gregoire $ i*)
+(*i $Id: pfedit.mli 9154 2006-09-20 17:18:18Z corbinea $ i*)
 
 (*i*)
 open Util
@@ -172,8 +172,12 @@ val make_focus : int -> unit
 val focus : unit -> int
 val focused_goal : unit -> int
 val subtree_solved : unit -> bool
+val tree_solved : unit -> bool
+val top_tree_solved : unit -> bool
 
 val reset_top_of_tree : unit -> unit
+val reset_top_of_script : unit -> unit
+
 val traverse : int -> unit
 val traverse_nth_goal : int -> unit
 val traverse_next_unproven : unit -> unit
diff --git a/proofs/proof_trees.ml b/proofs/proof_trees.ml
index 7e299b89..9d70d012 100644
--- a/proofs/proof_trees.ml
+++ b/proofs/proof_trees.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: proof_trees.ml 6113 2004-09-17 20:28:19Z barras $ *)
+(* $Id: proof_trees.ml 9154 2006-09-20 17:18:18Z corbinea $ *)
 
 open Closure
 open Util
@@ -18,6 +18,7 @@ open Sign
 open Evd
 open Environ
 open Evarutil
+open Decl_expr
 open Proof_type
 open Tacred
 open Typing
@@ -32,9 +33,9 @@ let is_bind = function
 
 (* Functions on goals *)
 
-let mk_goal hyps cl = 
+let mk_goal hyps cl extra = 
   { evar_hyps = hyps; evar_concl = cl; 
-    evar_body = Evar_empty}
+    evar_body = Evar_empty; evar_extra = extra }
 
 (* Functions on proof trees *)
 
@@ -52,7 +53,7 @@ let children_of_proof pf =
 let goal_of_proof pf = pf.goal
 
 let subproof_of_proof pf = match pf.ref with
-  | Some (Tactic (_,pf), _) -> pf
+  | Some (Nested (_,pf), _) -> pf
   | _ -> failwith "subproof_of_proof"
 
 let status_of_proof pf = pf.open_subgoals
@@ -62,7 +63,7 @@ let is_complete_proof pf = pf.open_subgoals = 0
 let is_leaf_proof pf = (pf.ref = None)
 
 let is_tactic_proof pf = match pf.ref with
-  | Some (Tactic _, _) -> true
+  | Some (Nested (Tactic _,_),_) -> true
   | _ -> false
 
 
@@ -72,6 +73,22 @@ let pf_lookup_name_as_renamed env ccl s =
 let pf_lookup_index_as_renamed env ccl n =
   Detyping.lookup_index_as_renamed env ccl n
 
+(* Functions on rules (Proof mode) *) 
+
+let is_dem_rule  = function
+    Decl_proof _  -> true
+  | _ -> false
+
+let is_proof_instr = function
+    Nested(Proof_instr (_,_),_) -> true
+  | _ -> false
+
+let is_focussing_command = function
+    Decl_proof b -> b 
+  | Nested (Proof_instr (b,_),_) -> b 
+  | _ -> false   
+
+
 (*********************************************************************)
 (*                  Pretty printing functions                        *)
 (*********************************************************************)
diff --git a/proofs/proof_trees.mli b/proofs/proof_trees.mli
index cbf91c8a..f9b64f41 100644
--- a/proofs/proof_trees.mli
+++ b/proofs/proof_trees.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: proof_trees.mli 7639 2005-12-02 10:01:15Z gregoire $ i*)
+(*i $Id: proof_trees.mli 9154 2006-09-20 17:18:18Z corbinea $ i*)
 
 (*i*)
 open Util
@@ -21,7 +21,7 @@ open Proof_type
 (* This module declares readable constraints, and a few utilities on
    constraints and proof trees *)
 
-val mk_goal : named_context_val -> constr -> goal
+val mk_goal : named_context_val -> constr -> Dyn.t option -> goal
 
 val rule_of_proof     : proof_tree -> rule
 val ref_of_proof      : proof_tree -> (rule * proof_tree list)
@@ -36,6 +36,8 @@ val is_tactic_proof   : proof_tree -> bool
 val pf_lookup_name_as_renamed  : env -> constr -> identifier -> int option
 val pf_lookup_index_as_renamed : env -> constr -> int -> int option
 
+val is_proof_instr : rule -> bool
+val is_focussing_command : rule -> bool
 
 (*s Pretty printing functions. *)
 
diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml
index 009e9d5b..abe31624 100644
--- a/proofs/proof_type.ml
+++ b/proofs/proof_type.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: proof_type.ml 7639 2005-12-02 10:01:15Z gregoire $ *)
+(*i $Id: proof_type.ml 9244 2006-10-16 17:11:44Z barras $ *)
 
 (*i*)
 open Environ
@@ -16,6 +16,7 @@ open Libnames
 open Term
 open Util
 open Tacexpr
+open Decl_expr
 open Rawterm
 open Genarg
 open Nametab
@@ -39,12 +40,6 @@ type prim_rule =
   | Move of bool * identifier * identifier
   | Rename of identifier * identifier
 
-(*s Proof trees. 
-  [ref] = [None] if the goal has still to be proved, 
-  and [Some (r,l)] if the rule [r] was applied to the goal
-  and gave [l] as subproofs to be completed. 
-  if [ref = (Some(Tactic (t,p),l))] then [p] is the proof 
-  that the goal can be proven if the goals in [l] are solved. *)
 type proof_tree = {
   open_subgoals : int;
   goal : goal;
@@ -52,9 +47,15 @@ type proof_tree = {
 
 and rule =
   | Prim of prim_rule
-  | Tactic of tactic_expr * proof_tree
+  | Nested of compound_rule * proof_tree 
+  | Decl_proof of bool
+  | Daimon
   | Change_evars
 
+and compound_rule=  
+  | Tactic of tactic_expr * bool
+  | Proof_instr of bool*proof_instr (* the boolean is for focus restrictions *)
+
 and goal = evar_info
 
 and tactic = goal sigma -> (goal list sigma * validation)
diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli
index 0e42dcba..d87c1298 100644
--- a/proofs/proof_type.mli
+++ b/proofs/proof_type.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: proof_type.mli 7639 2005-12-02 10:01:15Z gregoire $ i*)
+(*i $Id: proof_type.mli 9244 2006-10-16 17:11:44Z barras $ i*)
 
 (*i*)
 open Environ
@@ -16,6 +16,7 @@ open Libnames
 open Term
 open Util
 open Tacexpr
+open Decl_expr
 open Rawterm
 open Genarg
 open Nametab
@@ -46,7 +47,7 @@ type prim_rule =
              evar_body = Evar_Empty;
              evar_info = { pgm    : [The Realizer pgm if any]
                            lc     : [Set of evar num occurring in subgoal] }}
-   sigma = { stamp = [an int characterizing the ed field, for quick compare]
+   sigma = { stamp = [an int chardacterizing the ed field, for quick compare]
              ed : [A set of existential variables depending in the subgoal]
                number of first evar,
                it = { evar_concl = [the type of first evar]
@@ -71,7 +72,7 @@ type prim_rule =
   [ref] = [None] if the goal has still to be proved, 
   and [Some (r,l)] if the rule [r] was applied to the goal
   and gave [l] as subproofs to be completed. 
-  if [ref = (Some(Tactic (t,p),l))] then [p] is the proof 
+  if [ref = (Some(Nested(Tactic t,p),l))] then [p] is the proof 
   that the goal can be proven if the goals in [l] are solved. *)
 type proof_tree = {
   open_subgoals : int;
@@ -80,9 +81,16 @@ type proof_tree = {
 
 and rule =
   | Prim of prim_rule
-  | Tactic of tactic_expr * proof_tree
+  | Nested of compound_rule * proof_tree 
+  | Decl_proof of bool
+  | Daimon
   | Change_evars
 
+and compound_rule= 
+  (* the boolean of Tactic tells if the default tactic is used *)
+  | Tactic of tactic_expr * bool
+  | Proof_instr of bool * proof_instr
+
 and goal = evar_info
 
 and tactic = goal sigma -> (goal list sigma * validation)
diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml
index eb47fc2e..ad277caa 100644
--- a/proofs/redexpr.ml
+++ b/proofs/redexpr.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: redexpr.ml 8878 2006-05-30 16:44:25Z herbelin $ *)
+(* $Id: redexpr.ml 9058 2006-07-22 17:42:45Z bgregoir $ *)
 
 open Pp
 open Util
@@ -24,7 +24,7 @@ open RedFlags
 (* call by value normalisation function using the virtual machine *)
 let cbv_vm env _ c =
   let ctyp = (fst (Typeops.infer env c)).Environ.uj_type in
-  Vconv.cbv_vm env c ctyp
+  Vnorm.cbv_vm env c ctyp
 
 
 let set_opaque_const sp = 
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index 067ae471..70a0e3db 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: refiner.ml 8759 2006-04-28 12:24:14Z herbelin $ *)
+(* $Id: refiner.ml 9261 2006-10-23 10:01:40Z barras $ *)
 
 open Pp
 open Util
@@ -43,6 +43,31 @@ let and_status = List.fold_left (+) 0
 let pf_env gls = Global.env_of_context (sig_it gls).evar_hyps
 let pf_hyps gls = named_context_of_val (sig_it gls).evar_hyps
 
+
+let descend n p =
+  match p.ref with
+    | None        -> error "It is a leaf."
+    | Some(r,pfl) ->
+    	if List.length pfl >= n then
+	  (match list_chop (n-1) pfl with 
+	     | left,(wanted::right) ->
+		 (wanted,
+		  (fun pfl' ->
+                     if (List.length pfl' = 1) 
+		       & (List.hd pfl').goal = wanted.goal 
+		     then
+                       let pf'       = List.hd pfl' in
+                       let spfl      = left@(pf'::right) in
+                       let newstatus = and_status (List.map pf_status spfl) in
+                       { p with 
+			   open_subgoals = newstatus;
+			   ref           = Some(r,spfl) }
+                     else 
+		       error "descend: validation"))
+	     | _ -> assert false)
+    	else 
+	  error "Too few subproofs"
+
 (* Normalizing evars in a goal. Called by tactic Local_constraints
    (i.e. when the sigma of the proof tree changes). Detect if the
    goal is unchanged *)
@@ -50,10 +75,10 @@ let norm_goal sigma gl =
   let red_fun = Evarutil.nf_evar sigma in
   let ncl = red_fun gl.evar_concl in
   let ngl =
-    { evar_concl = ncl;
-      evar_hyps = map_named_val red_fun gl.evar_hyps; 
-      evar_body = gl.evar_body} in
-  if Evd.eq_evar_info ngl gl then None else Some ngl
+    { gl with 
+	evar_concl = ncl;
+	evar_hyps = map_named_val red_fun gl.evar_hyps } in
+    if Evd.eq_evar_info ngl gl then None else Some ngl
 
 
 (* [mapshape [ l1 ; ... ; lk ] [ v1 ; ... ; vk ] [ p_1 ; .... ; p_(l1+...+lk) ]]
@@ -91,9 +116,9 @@ let rec frontier p =
     	(List.flatten gll,
          (fun retpfl ->
             let pfl' = mapshape (List.map List.length gll) vl retpfl in
-            { open_subgoals = and_status (List.map pf_status pfl');
-              goal = p.goal;
-              ref = Some(r,pfl')}))
+              { p with
+		  open_subgoals = and_status (List.map pf_status pfl');
+		  ref = Some(r,pfl')}))
 
 
 let rec frontier_map_rec f n p =
@@ -111,9 +136,9 @@ let rec frontier_map_rec f n p =
             (fun (n,acc) p -> (n-p.open_subgoals,frontier_map_rec f n p::acc))
             (n,[]) pfl in
         let pfl' = List.rev rpfl' in
-        { open_subgoals = and_status (List.map pf_status pfl');
-          goal = p.goal;
-          ref = Some(r,pfl')}
+        { p with
+	    open_subgoals = and_status (List.map pf_status pfl');
+            ref = Some(r,pfl')}
 
 let frontier_map f n p =
   let nmax = p.open_subgoals in
@@ -137,9 +162,9 @@ let rec frontier_mapi_rec f i p =
             (fun (n,acc) p -> (n+p.open_subgoals,frontier_mapi_rec f n p::acc))
             (i,[]) pfl in
         let pfl' = List.rev rpfl' in
-        { open_subgoals = and_status (List.map pf_status pfl');
-          goal = p.goal;
-          ref = Some(r,pfl')}
+        { p with 
+	    open_subgoals = and_status (List.map pf_status pfl');
+            ref = Some(r,pfl')}
 
 let frontier_mapi f p = frontier_mapi_rec f 1 p
 
@@ -152,50 +177,35 @@ let rec nb_unsolved_goals pf = pf.open_subgoals
 
 (* leaf g is the canonical incomplete proof of a goal g *)
 
-let leaf g = {
-  open_subgoals = 1;
-  goal = g;
-  ref = None }
-
-(* Tactics table. *)
-
-let tac_tab = Hashtbl.create 17
-
-let add_tactic s t =
-  if Hashtbl.mem tac_tab s then
-    errorlabstrm ("Refiner.add_tactic: ") 
-      (str ("Cannot redeclare tactic "^s));
-  Hashtbl.add tac_tab s t
-
-let overwriting_add_tactic s t =
-  if Hashtbl.mem tac_tab s then begin
-    Hashtbl.remove tac_tab s;
-    warning ("Overwriting definition of tactic "^s)
-  end;
-  Hashtbl.add tac_tab s t
-
-let lookup_tactic s =
-  try 
-    Hashtbl.find tac_tab s
-  with Not_found -> 
-    errorlabstrm "Refiner.lookup_tactic"
-      (str"The tactic " ++ str s ++ str" is not installed")
-
+let leaf g = 
+  { open_subgoals = 1;
+    goal = g;
+    ref = None }
 
 (* refiner r is a tactic applying the rule r *)
 
 let check_subproof_connection gl spfl =
   list_for_all2eq (fun g pf -> Evd.eq_evar_info g pf.goal) gl spfl
 
-let abstract_tactic_expr te tacfun gls =
-  let (sgl_sigma,v) = tacfun gls in
-  let hidden_proof = v (List.map leaf sgl_sigma.it) in
+
+let abstract_operation syntax semantics gls =
+  let (sgl_sigma,validation) = semantics gls in
+  let hidden_proof = validation (List.map leaf sgl_sigma.it) in
   (sgl_sigma,
    fun spfl ->
      assert (check_subproof_connection sgl_sigma.it spfl);
      { open_subgoals = and_status (List.map pf_status spfl);
        goal = gls.it;
-       ref = Some(Tactic(te,hidden_proof),spfl) })
+       ref = Some(Nested(syntax,hidden_proof),spfl)})
+
+let abstract_tactic_expr ?(dflt=false) te tacfun gls =
+  abstract_operation (Tactic(te,dflt)) tacfun gls	
+
+let abstract_tactic ?(dflt=false) te =
+  abstract_tactic_expr ~dflt (Tacexpr.TacAtom (dummy_loc,te))
+
+let abstract_extended_tactic ?(dflt=false) s args = 
+  abstract_tactic ~dflt (Tacexpr.TacExtend (dummy_loc, s, args))
 
 let refiner = function
   | Prim pr as r ->
@@ -209,8 +219,21 @@ let refiner = function
                goal = goal_sigma.it;
                ref = Some(r,spfl) })))
 
-  | Tactic _ -> failwith "Refiner: should not occur"
+
+  | Nested (_,_) | Decl_proof _ -> 
+      failwith "Refiner: should not occur"
       
+	(* Daimon is a canonical unfinished proof *)
+
+  | Daimon -> 
+      fun gls -> 
+	({it=[];sigma=gls.sigma},  
+	 fun spfl -> 
+	   assert (spfl=[]);
+	   { open_subgoals = 0;
+             goal = gls.it;
+             ref = Some(Daimon,[])})
+
    (* [Local_constraints lc] makes the local constraints be [lc] and
       normalizes evars *)
 
@@ -237,19 +260,11 @@ let local_Constraints gl = refiner Change_evars gl
 
 let norm_evar_tac = local_Constraints
 
-(*
-let vernac_tactic (s,args) =
-  let tacfun = lookup_tactic s args in
-  abstract_extra_tactic s args tacfun
-*)
-let abstract_tactic te = abstract_tactic_expr (Tacexpr.TacAtom (dummy_loc,te))
-
-let abstract_extended_tactic s args = 
-  abstract_tactic (Tacexpr.TacExtend (dummy_loc, s, args))
-
-let vernac_tactic (s,args) =
-  let tacfun = lookup_tactic s args in
-  abstract_extended_tactic s args tacfun
+let norm_evar_proof sigma pf =
+  let nf_subgoal i sgl =
+    let (gll,v) = norm_evar_tac {it=sgl.goal;sigma=sigma} in
+    v (List.map leaf gll.it) in
+  frontier_mapi nf_subgoal pf
 
 (* [extract_open_proof : proof_tree -> constr * (int * constr) list]
   takes a (not necessarly complete) proof and gives a pair (pfterm,obl)
@@ -271,14 +286,16 @@ let extract_open_proof sigma pf =
   let rec proof_extractor vl = function
     | {ref=Some(Prim _,_)} as pf -> prim_extractor proof_extractor vl pf
 	  
-    | {ref=Some(Tactic (_,hidden_proof),spfl)} ->
+    | {ref=Some(Nested(_,hidden_proof),spfl)} ->
 	let sgl,v = frontier hidden_proof in
 	let flat_proof = v spfl in
 	proof_extractor vl flat_proof
-	  
+ 
     | {ref=Some(Change_evars,[pf])} -> (proof_extractor vl) pf
+
+    | {ref=Some(Decl_proof _,[pf])} -> (proof_extractor vl) pf
 	  
-    | {ref=None;goal=goal} ->
+    | {ref=(None|Some(Daimon,[]));goal=goal} ->
 	let visible_rels =
           map_succeed
             (fun id ->
@@ -555,6 +572,8 @@ let tclIFTHENSELSE=ite_gen tclTHENS
 
 let tclIFTHENSVELSE=ite_gen tclTHENSV
 
+let tclIFTHENTRYELSEMUST tac1 tac2 gl = 
+  tclIFTHENELSE tac1 (tclTRY tac2) tac2 gl
 
 (* Fails if a tactic did not solve the goal *)
 let tclCOMPLETE tac = tclTHEN tac (tclFAIL_s "Proof is not complete.")
@@ -633,7 +652,6 @@ let tactic_list_tactic tac gls =
 
 
 
-
 (* The type of proof-trees state and a few utilities 
    A proof-tree state is built from a proof-tree, a set of global
    constraints, and a stack which allows to navigate inside the
@@ -665,41 +683,19 @@ let nth_goal_of_pftreestate n pts =
   try {it = List.nth goals (n-1); sigma = pts.tpfsigma }
   with Invalid_argument _ | Failure _ -> non_existent_goal n
 
-let descend n p =
-  match p.ref with
-    | None        -> error "It is a leaf."
-    | Some(r,pfl) ->
-    	if List.length pfl >= n then
-	  (match list_chop (n-1) pfl with 
-	     | left,(wanted::right) ->
-		 (wanted,
-		  (fun pfl' ->
-                     if (List.length pfl' = 1) 
-		       & (List.hd pfl').goal = wanted.goal 
-		     then
-                       let pf'       = List.hd pfl' in
-                       let spfl      = left@(pf'::right) in
-                       let newstatus = and_status (List.map pf_status spfl) in
-                       { open_subgoals = newstatus;
-			 goal          = p.goal;
-			 ref           = Some(r,spfl) }
-                     else 
-		       error "descend: validation"))
-	     | _ -> assert false)
-    	else 
-	  error "Too few subproofs"
-
 let traverse n pts = match n with 
   | 0 -> (* go to the parent *)
       (match  pts.tstack with
 	 | [] -> error "traverse: no ancestors"
 	 | (_,v)::tl ->
-	     { tpf = v [pts.tpf];
+             let pf = v [pts.tpf] in
+             let pf = norm_evar_proof pts.tpfsigma pf in
+	     { tpf = pf;
 	       tstack = tl;
 	       tpfsigma = pts.tpfsigma })
   | -1 -> (* go to the hidden tactic-proof, if any, otherwise fail *)
       (match pts.tpf.ref with
-	 | Some (Tactic (_,spf),_) ->
+	 | Some (Nested (_,spf),_) ->
 	     let v = (fun pfl -> pts.tpf) in 
 	     { tpf = spf;
                tstack = (-1,v)::pts.tstack;
@@ -718,17 +714,23 @@ let app_tac sigr tac p =
   sigr := gll.sigma;
   v (List.map leaf gll.it)
 
-(* solve the nth subgoal with tactic tac *)
-let solve_nth_pftreestate n tac pts =
+(* modify proof state at current position *)
+
+let map_pftreestate f pts =
   let sigr = ref pts.tpfsigma in
-  let tpf' = frontier_map (app_tac sigr tac) n pts.tpf in
+  let tpf' = f sigr pts.tpf in
   let tpf'' =
-    if !sigr == pts.tpfsigma then tpf'
-    else frontier_mapi (fun _ g -> app_tac sigr norm_evar_tac g) tpf' in
+    if !sigr == pts.tpfsigma then tpf' else norm_evar_proof !sigr tpf' in
   { tpf      = tpf'';
     tpfsigma = !sigr;
     tstack   = pts.tstack }
 
+(* solve the nth subgoal with tactic tac *)
+
+let solve_nth_pftreestate n tac =
+  map_pftreestate 
+    (fun sigr pt -> frontier_map (app_tac sigr tac) n pt)
+ 
 let solve_pftreestate = solve_nth_pftreestate 1
 
 (* This function implements a poor man's undo at the current goal.
@@ -880,6 +882,38 @@ let prev_unproven pts =
 let rec top_of_tree pts = 
   if is_top_pftreestate pts then pts else top_of_tree(traverse 0 pts)
 
+let change_rule f pts =
+  let mark_top _ pt =
+    match pt.ref with
+	Some (oldrule,l) -> 
+	  {pt with ref=Some (f oldrule,l)}
+      | _ -> invalid_arg "change_rule" in
+    map_pftreestate mark_top pts
+
+let match_rule p pts =
+  match (proof_of_pftreestate pts).ref with
+      Some (r,_) -> p r
+    | None -> false
+
+let rec up_until_matching_rule p pts = 
+  if is_top_pftreestate pts then 
+    raise Not_found
+  else
+    let one_up = traverse 0 pts in
+      if match_rule p one_up then 
+	pts
+      else
+	up_until_matching_rule p one_up
+
+let rec up_to_matching_rule p pts = 
+  if match_rule p pts then 
+    pts
+  else
+    if is_top_pftreestate pts then 
+      raise Not_found
+    else
+      let one_up = traverse 0 pts in
+      	up_to_matching_rule p one_up
 
 (* Change evars *)
 let tclEVARS sigma gls = tclIDTAC {gls with sigma=sigma}
diff --git a/proofs/refiner.mli b/proofs/refiner.mli
index 417ddbcd..d8b13dba 100644
--- a/proofs/refiner.mli
+++ b/proofs/refiner.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: refiner.mli 7911 2006-01-21 11:18:36Z herbelin $ i*)
+(*i $Id: refiner.mli 9244 2006-10-16 17:11:44Z barras $ i*)
 
 (*i*)
 open Term
@@ -32,20 +32,17 @@ val apply_sig_tac :
 
 type transformation_tactic = proof_tree -> (goal list * validation)
 
-val add_tactic             : string -> (closed_generic_argument list -> tactic) -> unit
-val overwriting_add_tactic : string -> (closed_generic_argument list -> tactic) -> unit
-val lookup_tactic          : string -> (closed_generic_argument list) -> tactic
-
 (*s Hiding the implementation of tactics. *)
 
 (* [abstract_tactic tac] hides the (partial) proof produced by [tac] under
-   a single proof node *)
-val abstract_tactic : atomic_tactic_expr -> tactic -> tactic
-val abstract_tactic_expr : tactic_expr -> tactic -> tactic
-val abstract_extended_tactic : string -> closed_generic_argument list -> tactic -> tactic
+   a single proof node. The boolean tells if the default tactic is used. *)
+val abstract_operation : compound_rule -> tactic -> tactic
+val abstract_tactic : ?dflt:bool -> atomic_tactic_expr -> tactic -> tactic
+val abstract_tactic_expr : ?dflt:bool -> tactic_expr -> tactic -> tactic
+val abstract_extended_tactic :
+  ?dflt:bool -> string -> closed_generic_argument list -> tactic -> tactic
 
 val refiner : rule -> tactic
-val vernac_tactic : string * closed_generic_argument list -> tactic
 val frontier : transformation_tactic
 val list_pf : proof_tree -> goal list
 val unTAC : tactic -> goal sigma -> proof_tree sigma
@@ -148,6 +145,12 @@ val tclIFTHENELSE    : tactic -> tactic -> tactic -> tactic
 val tclIFTHENSELSE   : tactic -> tactic list -> tactic ->tactic
 val tclIFTHENSVELSE   : tactic -> tactic array -> tactic ->tactic
 
+(* [tclIFTHENTRYELSEMUST tac1 tac2 gls] applies [tac1] then [tac2]. If [tac1]
+   has been successful, then [tac2] may fail. Otherwise, [tac2] must succeed. 
+   Equivalent to [(tac1;try tac2)||tac2] *)
+
+val tclIFTHENTRYELSEMUST : tactic -> tactic -> tactic
+
 (*s Tactics handling a list of goals. *)
 
 type validation_list = proof_tree list -> proof_tree list
@@ -170,11 +173,14 @@ type pftreestate
 val proof_of_pftreestate : pftreestate -> proof_tree
 val cursor_of_pftreestate : pftreestate -> int list
 val is_top_pftreestate : pftreestate -> bool
+val match_rule : (rule -> bool) -> pftreestate -> bool
 val evc_of_pftreestate : pftreestate -> evar_map
 val top_goal_of_pftreestate : pftreestate -> goal sigma
 val nth_goal_of_pftreestate : int -> pftreestate -> goal sigma
 
 val traverse : int -> pftreestate -> pftreestate
+val map_pftreestate : 
+  (evar_map ref -> proof_tree -> proof_tree) -> pftreestate -> pftreestate
 val solve_nth_pftreestate : int -> tactic -> pftreestate -> pftreestate
 val solve_pftreestate : tactic -> pftreestate -> pftreestate
 
@@ -193,6 +199,12 @@ val node_next_unproven : int -> pftreestate -> pftreestate
 val next_unproven : pftreestate -> pftreestate
 val prev_unproven : pftreestate -> pftreestate
 val top_of_tree : pftreestate -> pftreestate
+val match_rule : (rule -> bool) -> pftreestate -> bool
+val up_until_matching_rule : (rule -> bool) -> 
+  pftreestate -> pftreestate
+val up_to_matching_rule : (rule -> bool) -> 
+  pftreestate -> pftreestate
+val change_rule : (rule -> rule) -> pftreestate -> pftreestate
 val change_constraints_pftreestate 
   : evar_map -> pftreestate -> pftreestate
 
diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml
index b721dacd..0fe21552 100644
--- a/proofs/tacexpr.ml
+++ b/proofs/tacexpr.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: tacexpr.ml 8917 2006-06-07 16:59:05Z herbelin $ i*)
+(*i $Id: tacexpr.ml 9267 2006-10-24 12:55:46Z herbelin $ i*)
 
 open Names
 open Topconstr
@@ -234,7 +234,7 @@ and ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_arg =
       'ref * ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_arg list
   | TacExternal of loc * string * string * 
       ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_arg list
-  | TacFreshId     of string option
+  | TacFreshId     of string or_var list
   | Tacexp of 'tac
 
 (* Globalized tactics *)
diff --git a/proofs/tactic_debug.ml b/proofs/tactic_debug.ml
index 889e06a8..96df8f64 100644
--- a/proofs/tactic_debug.ml
+++ b/proofs/tactic_debug.ml
@@ -31,6 +31,8 @@ type debug_info =
 (* An exception handler *)
 let explain_logic_error = ref (fun e -> mt())
 
+let explain_logic_error_no_anomaly = ref (fun e -> mt())
+
 (* Prints the goal *)
 let db_pr_goal g =
   msgnl (str "Goal:" ++ fnl () ++ Proof_trees.db_pr_goal (Refiner.sig_it g))
diff --git a/proofs/tactic_debug.mli b/proofs/tactic_debug.mli
index fc1b6120..6de8244d 100644
--- a/proofs/tactic_debug.mli
+++ b/proofs/tactic_debug.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: tactic_debug.mli 7911 2006-01-21 11:18:36Z herbelin $ i*)
+(*i $Id: tactic_debug.mli 9092 2006-08-28 11:42:14Z bertot $ i*)
 
 open Environ
 open Pattern
@@ -66,5 +66,11 @@ val db_eval_failure : debug_info -> Pp.std_ppcmds -> unit
 (* An exception handler *)
 val explain_logic_error: (exn -> Pp.std_ppcmds) ref
 
+(* For use in the Ltac debugger: some exception that are usually
+   consider anomalies are acceptable because they are caught later in
+   the process that is being debugged.  One should not require
+   from users that they report these anomalies. *)
+val explain_logic_error_no_anomaly : (exn -> Pp.std_ppcmds) ref
+
 (* Prints a logic failure message for a rule *)
 val db_logic_failure : debug_info -> exn -> unit