Declarative Proof Language: main commit

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9154 85f007b7-540e-0410-9357-904b9bb8a0f7

14 files changed, 473 insertions, 50 deletions

diff --git a/proofs/decl_expr.mli b/proofs/decl_expr.mli
new file mode 100644
index 0000000000..24af3842cb
--- /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 0000000000..094c562532
--- /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 0000000000..0dd1cb33c3
--- /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 d5ea25bd30..b0f933a504 100644
--- a/proofs/evar_refiner.ml
+++ b/proofs/evar_refiner.ml
@@ -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 090671e046..7b9da802c1 100644
--- a/proofs/evar_refiner.mli
+++ b/proofs/evar_refiner.mli
@@ -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 209c3bb65f..b5c8011051 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -88,7 +88,7 @@ let clear_hyps ids gl =
         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
+  mk_goal nhyps ncl gl.evar_extra
 
 (* The ClearBody tactic *)
 
@@ -264,6 +264,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 	
@@ -315,6 +316,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;
@@ -392,6 +394,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 ->
@@ -474,7 +477,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 f724589f69..c6cb86dc92 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -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 8871e7e00c..c3d531c692 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -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 73cc5d2736..c7a32682aa 100644
--- a/proofs/proof_trees.ml
+++ b/proofs/proof_trees.ml
@@ -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 1b691e2584..dcbddbd9e8 100644
--- a/proofs/proof_trees.mli
+++ b/proofs/proof_trees.mli
@@ -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 db3c0e7e25..4037237026 100644
--- a/proofs/proof_type.ml
+++ b/proofs/proof_type.ml
@@ -16,6 +16,7 @@ open Libnames
 open Term
 open Util
 open Tacexpr
+open Decl_expr
 open Rawterm
 open Genarg
 open Nametab
@@ -52,9 +53,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
+  | 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 e222730582..74c36c9811 100644
--- a/proofs/proof_type.mli
+++ b/proofs/proof_type.mli
@@ -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]
@@ -80,9 +81,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
+  | Proof_instr of bool * proof_instr
+
 and goal = evar_info
 
 and tactic = goal sigma -> (goal list sigma * validation)
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index ee4b672a18..48c9238e05 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -50,10 +50,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 +91,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 +111,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 +137,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,10 +152,10 @@ 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 }
+let leaf g = 
+  { open_subgoals = 1;
+    goal = g;
+    ref = None }
 
 (* Tactics table. *)
 
@@ -187,15 +187,19 @@ let lookup_tactic s =
 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 te tacfun gls =
+  abstract_operation (Tactic te) tacfun gls	
 
 let refiner = function
   | Prim pr as r ->
@@ -209,8 +213,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 *)
 
@@ -271,14 +288,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 ->
@@ -680,9 +699,9 @@ let descend n p =
                        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) }
+                       { p with 
+			   open_subgoals = newstatus;
+			   ref           = Some(r,spfl) }
                      else 
 		       error "descend: validation"))
 	     | _ -> assert false)
@@ -699,7 +718,7 @@ let traverse n pts = match n with
 	       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,10 +737,11 @@ 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
@@ -729,6 +749,12 @@ let solve_nth_pftreestate n tac pts =
     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 +906,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 41b312e5db..097ff99a93 100644
--- a/proofs/refiner.mli
+++ b/proofs/refiner.mli
@@ -40,6 +40,7 @@ val lookup_tactic          : string -> (closed_generic_argument list) -> tactic
 
 (* [abstract_tactic tac] hides the (partial) proof produced by [tac] under
    a single proof node *)
+val abstract_operation : compound_rule -> tactic -> tactic
 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
@@ -170,11 +171,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 +197,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