Nettoyage de l'interface de Pfedit

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

19 files changed, 296 insertions, 184 deletions

diff --git a/dev/changements.txt b/dev/changements.txt
index 450ee1bd50..8d028c2359 100644
--- a/dev/changements.txt
+++ b/dev/changements.txt
@@ -106,6 +106,13 @@ Changements dans les fonctions :
         Divers
           initial_sign -> var_context
 
+        Pfedit
+	  list_proofs -> get_all_proof_names
+          get_proof -> get_current_proof_name
+          abort_cur_goal -> abort_current_goal
+          get_evmap_sign -> get_goal_context/get_current_goal_context
+          unset_undo -> reset_undo
+
 Changements dans les inductifs
 ------------------------------
 Nouveaux types "constructor" et "inductive" dans Term
diff --git a/lib/edit.ml b/lib/edit.ml
index 7ff552ef6f..ae54d71da5 100644
--- a/lib/edit.ml
+++ b/lib/edit.ml
@@ -20,7 +20,7 @@ let focus e nd =
     | Some f -> if not (Hashtbl.mem e.buf f) then invalid_arg "Edit.focus"
   end;
   begin match e.focus with
-    | None -> ()
+    | None -> if nd = None then warning "There is already no focused proof"
     | Some foc -> 
 	if e.focus <> nd then
           e.last_focused_stk <- foc::(list_except foc e.last_focused_stk)
diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml
index 91a83ea9d9..004bc5c474 100644
--- a/proofs/evar_refiner.ml
+++ b/proofs/evar_refiner.ml
@@ -162,3 +162,36 @@ let w_Define sp c wc =
     	in 
 	(ids_mod (fun evc -> (Proof_trees.remap evc (sp,spdecl'))) wc)
     | _ -> error "define_evar"
+
+(******************************************)
+(* Instantiation of existential variables *)
+(******************************************)
+
+let instantiate_pf n c pfts = 
+  let gls = top_goal_of_pftreestate pfts in
+  let (wc,_) = startWalk gls in
+  let sigma  = (w_Underlying wc) in 
+  let (sp,_) = 
+    try 
+      List.nth (Evd.non_instantiated sigma) (n-1)
+    with Failure _ -> 
+      error "not so many uninstantiated existential variables"
+  in 
+  let wc' = w_Define sp c wc in 
+  let newgc = ts_mk (w_Underlying wc') in 
+  change_constraints_pftreestate newgc pfts
+
+let instantiate_pf_com n com pfts = 
+  let gls = top_goal_of_pftreestate pfts in
+  let (wc,_) = startWalk gls in
+  let sigma = (w_Underlying wc) in 
+  let (sp,evd) = 
+    try
+      List.nth (Evd.non_instantiated sigma) (n-1) 
+    with Failure _ -> 
+      error "not so many uninstantiated existential variables"
+  in 
+  let c = Astterm.interp_constr sigma evd.evar_env com in     
+  let wc' = w_Define sp c wc in
+  let newgc = ts_mk (w_Underlying wc') in
+  change_constraints_pftreestate newgc pfts
diff --git a/proofs/evar_refiner.mli b/proofs/evar_refiner.mli
index 1674f2f3ac..ef72c9d35d 100644
--- a/proofs/evar_refiner.mli
+++ b/proofs/evar_refiner.mli
@@ -49,3 +49,6 @@ val w_ORELSE     : w_tactic -> w_tactic -> w_tactic
 val ctxt_type_of : readable_constraints -> constr -> constr
 
 val evars_of     : readable_constraints -> constr -> local_constraints
+
+val instantiate_pf     : int -> constr -> pftreestate -> pftreestate
+val instantiate_pf_com : int -> Coqast.t -> pftreestate -> pftreestate
diff --git a/proofs/logic.ml b/proofs/logic.ml
index 3270177ee1..2d4e8a903b 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -123,7 +123,7 @@ and mk_casegoals sigma goal goalacc p c =
   let (acc',ct) = mk_hdgoals sigma goal goalacc c in 
   let (acc'',pt) = mk_hdgoals sigma goal acc' p in
   let indspec =
-    try try_mutind_of env sigma ct
+    try find_inductive env sigma ct
     with Induc -> anomaly "mk_casegoals" in
   let (lbrty,conclty) = type_case_branches env sigma indspec pt p c in
   (acc'',lbrty,conclty)
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index 7ffb408786..44c4fc5fb7 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -25,13 +25,14 @@ type proof_topstate = {
 
 let proof_edits = (Edit.empty() : (string,pftreestate,proof_topstate) Edit.t)
 
-let list_proofs () = Edit.dom proof_edits
+let get_all_proof_names () = Edit.dom proof_edits
 
 let msg_proofs use_resume =
   match Edit.dom proof_edits with
     | [] -> [< 'sPC ; 'sTR"(No proof-editing in progress)." >]
     | l ->  [< 'sTR"." ; 'fNL ; 'sTR"Proofs currently edited:" ; 'sPC ;
-               (prlist_with_sep pr_spc pr_str (list_proofs ())) ; 'sTR"." ;
+               (prlist_with_sep pr_spc pr_str (get_all_proof_names ())) ;
+	       'sTR"." ;
                (if use_resume then [< 'fNL ; 'sTR"Use \"Resume\" first." >]
               	else [< >])
             >]
@@ -52,6 +53,7 @@ let get_state () =
 let get_topstate ()    = snd(get_state())
 let get_pftreestate () = fst(get_state())
 
+(*
 let get_evmap_sign og =
   let og = match og with
     | Some n ->
@@ -67,22 +69,30 @@ let get_evmap_sign og =
   match og with
     | Some goal -> (project goal, pf_env goal)
     | _ -> (Evd.empty, Global.env())
- 
-let set_proof s = 
+*)
+
+let get_goal_context n =
+  let pftree = get_pftreestate () in
+  let goal = nth_goal_of_pftreestate n pftree in
+  (project goal, pf_env goal)
+
+let get_current_goal_context () = get_goal_context 1
+
+let set_current_proof s = 
   try 
     Edit.focus proof_edits s
   with Invalid_argument "Edit.focus" ->
     errorlabstrm "Pfedit.set_proof"
       [< 'sTR"No such proof" ; (msg_proofs false) >]
       
-let resume_last () =
+let resume_last_proof () =
   match (Edit.last_focused proof_edits) with
     | None ->
         errorlabstrm "resume_last" [< 'sTR"No proof-editing in progress." >]
     | p -> 
 	Edit.focus proof_edits p
 	  
-let get_proof () =
+let get_current_proof_name () =
   match Edit.read proof_edits with
     | None ->
         errorlabstrm "Pfedit.get_proof"
@@ -108,13 +118,6 @@ let mutate f =
     errorlabstrm "Pfedit.mutate"
       [< 'sTR"No focused proof" ; msg_proofs true >]
 
-let rev_mutate f =
-  try 
-    Edit.mutate proof_edits (fun _ pfs -> f pfs)
-  with Invalid_argument "Edit.rev_mutate" ->
-    errorlabstrm "Pfedit.rev_mutate"
-      [< 'sTR"No focused proof"; msg_proofs true >]
-
 let start (na,ts) =
   let pfs = mk_pftreestate ts.top_goal in 
   add_proof(na,pfs,ts)
@@ -127,13 +130,8 @@ let restart () =
     | Some(na,_,ts) -> 
 	del_proof na;
         start (na,ts);
-        set_proof (Some na)
+        set_current_proof (Some na)
 
-let proof_prompt () =
-  match Edit.read proof_edits with
-    | None -> "Coq < "
-    | Some(na,_,_) -> na^" < "
-	  
 let proof_term () =
   extract_pftreestate (get_pftreestate())
     
@@ -153,7 +151,7 @@ let set_undo n =
   else 
     error "Cannot set a negative undo limit"
       
-let unset_undo  () = set_undo undo_default
+let reset_undo  () = set_undo undo_default
 
 let undo n =
   try 
@@ -171,7 +169,7 @@ let undo n =
 
 let save_named opacity =
   let (pfs,ts) = get_state() 
-  and ident = get_proof() in
+  and ident = get_current_proof_name () in
   let {evar_concl=concl} = ts.top_goal 
   and strength = ts.top_strength in
   let pfterm = extract_pftreestate pfs in 
@@ -181,11 +179,11 @@ let save_named opacity =
   del_proof ident;
   if Options.is_verbose() then message (ident ^ " is defined")
     
-let save_anonymous opacity save_ident n =
+let save_anonymous opacity save_ident strength =
   let (pfs,ts) = get_state() 
-  and ident = get_proof() in
-  let {evar_concl=concl} = ts.top_goal 
-  and strength = ts.top_strength in
+  and ident = get_current_proof_name() in
+  let {evar_concl=concl} = ts.top_goal in
+  (* we do not consider default ts.top_strength *)
   let pfterm = extract_pftreestate pfs in 
   if ident = "Unnamed_thm" then
     declare_constant (id_of_string save_ident)
@@ -213,28 +211,23 @@ let save_anonymous_remark opacity id =
  
 let refining () = [] <> (Edit.dom proof_edits)
 
-let abort_goal pn = del_proof pn
-
-let abort_cur_goal () = del_proof (get_proof ())
+let check_no_pending_proofs () =
+  if refining () then 
+    errorlabstrm "check_no_pending_proofs"
+      [< 'sTR"Proof editing in progress" ; (msg_proofs false) ;
+         'sTR"Use \"Abort All\" first or complete proof(s)." >]
 
-let abort_goals () =
-  if refining() then begin
-    init_proofs();
-    message "Current goals aborted"
-  end else 
-    error "No proof-editing in progress"
+let abort_goal pn = del_proof pn
 
-let abort_refine f x = 
-  if refining() then abort_goals(); 
-  f x
-  (* used to be: error "Must save or abort current goal first" *)
+let abort_current_goal () = del_proof (get_current_proof_name ())
 
+let abort_goals = init_proofs
    
 (*********************************************************************)
 (*              Modifying the current prooftree                      *)
 (*********************************************************************)
 
-let start_proof_with_type na str env concl =
+let start_proof na str env concl =
   let top_goal = mk_goal (mt_ctxt Intset.empty) env concl in
   let ts = { 
     top_hyps = (env,empty_env);
@@ -242,19 +235,17 @@ let start_proof_with_type na str env concl =
     top_strength = str }
   in
   start(na,ts);
-  set_proof (Some na)
-
-let start_proof na str concl_com =
-  let sigma = Evd.empty in
-  let env = Global.env() in
-  let concl = interp_type sigma env concl_com in
-  start_proof_with_type na str env concl
+  set_current_proof (Some na)
 
+(*
 let start_proof_constr na str concl =
   let sigma = Evd.empty in
   let env = Global.env() in
+(* Si c'est un constr, il est supposé typable dans le contexte courant
   let _ = execute_type env sigma concl in
+*)
   start_proof_with_type na str env concl
+*)
 
 let solve_nth k tac =
   let pft = get_pftreestate() in
@@ -273,7 +264,9 @@ let solve_nth k tac =
 
 let by tac = mutate (solve_pftreestate tac)
 
-let traverse n = rev_mutate (traverse n)
+let instantiate_nth_evar_com n c = mutate (instantiate_pf_com n c)
+
+let traverse n = mutate (traverse n)
  
 (* [traverse_to path]
 
@@ -338,15 +331,25 @@ let traverse_to path =
     let down_list, up_count = common_ancestor path cursor in
     traverse_down down_list (traverse_up up_count pfs)
   in
-  rev_mutate (up_and_down path)
+  mutate (up_and_down path)
 
 (* traverse the proof tree until it reach the nth subgoal *)
 let traverse_nth_goal n = mutate (nth_unproven n)
 
+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
 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
+
+
 
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index 3499f9227b..6d5c56439a 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -12,59 +12,152 @@ open Proof_type
 open Tacmach
 (*i*)
 
-val proof_prompt : unit -> string
+(* [refining ()] tells if there is some proof in progress, even if a not
+   focused one *)
+
 val refining : unit -> bool
+
+(* [check_no_pending_proofs ()] fails if there is still some proof in
+   progress *)
+
+val check_no_pending_proofs : unit -> unit
+
+(* [abort_goal name] aborts proof of name [name] or failed if no proof
+has this name *)
+
 val abort_goal : string -> unit
-val abort_cur_goal : unit -> unit
+
+(* [abort_current_goal ()] aborts current focused proof or failed if
+    no proof is focused *)
+
+val abort_current_goal : unit -> unit
+
+(* [abort_goals ()] aborts all open proofs if any *)
+
 val abort_goals : unit -> unit
-val abort_refine : ('a -> 'b) -> 'a -> 'b
-val msg_proofs : bool -> std_ppcmds
 
-val undo_limit : int ref
-val set_undo : int -> unit
-val unset_undo : unit -> unit
+(* [undo n] undoes the effect of the last [n] tactics applied to the
+    current proof; it fails if no proof is focused or if the ``undo''
+    stack is exhausted *)
+
 val undo : int -> unit
-val resume_last : unit -> unit
 
-type proof_topstate = {
-  top_hyps : env * env;
-  top_goal : goal;
-  top_strength : strength }
+(* [set_undo n] sets the size of the ``undo'' stack *)
+
+val set_undo : int -> unit
+
+(* [reset_undo n] sets the size of the ``undo'' stack to the default
+   value (12) *)
+
+val reset_undo : unit -> unit
+
+(* [resume_last_proof ()] focus on the last unfocused proof or fails
+   if there is no suspended proofs *)
+
+val resume_last_proof : unit -> unit
+
+(* [get_pftreestate ()] returns the current focused pending proof or
+   raises [UserError "no focused proof"] *)
 
-val get_state : unit -> pftreestate * proof_topstate
-val get_topstate : unit -> proof_topstate
 val get_pftreestate : unit -> pftreestate
-val get_evmap_sign : int option -> evar_declarations * env
-val set_proof : string option -> unit
-val get_proof : unit -> string
-val list_proofs : unit -> string list
-val add_proof : string * pftreestate * proof_topstate -> unit
-val del_proof : string -> unit
-val init_proofs : unit -> unit
 
-val mutate : (pftreestate -> pftreestate) -> unit
-val rev_mutate : (pftreestate -> pftreestate) -> unit
-val start : string * proof_topstate -> unit
+(* [get_goal_context n] returns the context of the [n]th subgoal of
+   the current focused proof or raises a [UserError] if there is no
+   focused proof or if there is no more subgoals *)
+
+val get_goal_context : int -> evar_declarations * env
+
+(* [get_current_goal_context ()] works as [get_goal_context 1] *)
+
+val get_current_goal_context : unit -> evar_declarations * env
+
+(* [set_current_proof None] unfocuses the current focused proof; [set_proof
+(Some name)] focuses on the proof of name [name] or raises a
+[UserError] if no proof has name [name] *)
+
+val set_current_proof : string option -> unit
+
+(* [get_current_proof_name ()] return the name of the current focused
+    proof or failed if no proof is focused *)
+
+val get_current_proof_name : unit -> string
+
+(* [list_proofs ()] returns the list of all pending proof names *)
+
+val get_all_proof_names : unit -> string list
+
+(* [restart ()] restarts the current focused proof from the beginning
+   or fails if no proof is focused *)
+
 val restart : unit -> unit
-val proof_prompt : unit -> string
-val proof_term : unit -> constr
 
-val start_proof : string -> strength -> Coqast.t -> unit
-val start_proof_constr : string -> strength -> constr -> unit
+(* [start_proof s str env t] starts a proof of name [s] and conclusion [t] *)
+
+val start_proof : string -> strength -> env -> constr -> unit
+
+(* [save_named b] saves the current completed proof under the name it
+was started; boolean [b] tells if the theorem is declared opaque; it
+fails if the proof is not completed *)
 
 val save_named : bool -> unit
-val save_anonymous : bool -> string -> 'a -> unit
+
+(* [save_anonymous_thm b name] behaves as [save_named] but declares the
+theorem under the name [name] and gives it the strength of a theorem *)
+
 val save_anonymous_thm : bool -> string -> unit
+
+(* [save_anonymous_remark b name] behaves as [save_named] but declares the
+theorem under the name [name] and gives it the strength of a remark *)
+
 val save_anonymous_remark : bool -> string -> unit
 
+(* [solve_nth n tac] applies tactic [tac] to the [n]th subgoal of the
+   current focused proof or raises a UserError if no proof is focused or
+   if there is no [n]th subgoal *)
+
 val solve_nth : int -> tactic -> unit
+
+(* [by tac] applies tactic [tac] to the 1st subgoal of the current
+   focused proof or raises a UserError if there is no focused proof or
+   if there is no more subgoals *)
+
 val by : tactic -> unit
-val traverse : int -> unit
-val traverse_nth_goal : int -> unit
-val traverse_to : int list -> unit
+
+(* [instantiate_nth_evar_com n c] instantiate the [n]th undefined
+   existential variable of the current focused proof by [c] or raises a
+   UserError if no proof is focused or if there is no such [n]th
+   existential variable *)
+
+val instantiate_nth_evar_com : int -> Coqast.t -> unit
+
+(* To deal with focus *)
 
 val make_focus : int -> unit
 val focus : unit -> int
 val focused_goal : unit -> int
-
 val subtree_solved : unit -> bool
+
+val reset_top_of_tree : unit -> unit
+val traverse : int -> unit
+val traverse_nth_goal : int -> unit
+val traverse_next_unproven : unit -> unit
+val traverse_prev_unproven : unit -> unit
+
+(*i N'ont pas à être exportées
+type proof_topstate
+val msg_proofs : bool -> std_ppcmds
+val undo_limit : int ref
+val get_state : unit -> pftreestate * proof_topstate
+val get_topstate : unit -> proof_topstate
+val add_proof : string * pftreestate * proof_topstate -> unit
+val del_proof : string -> unit
+val init_proofs : unit -> unit
+
+val mutate : (pftreestate -> pftreestate) -> unit
+val rev_mutate : (pftreestate -> pftreestate) -> unit
+val start : string * proof_topstate -> unit
+val proof_term : unit -> constr
+val save_anonymous : bool -> string -> unit
+val traverse_to : int list -> unit
+i*)
+
diff --git a/proofs/refiner.mli b/proofs/refiner.mli
index d0b3ca33ab..4b821596e4 100644
--- a/proofs/refiner.mli
+++ b/proofs/refiner.mli
@@ -97,6 +97,7 @@ val nth_goal_of_pftreestate : int -> pftreestate -> goal sigma
 val traverse : int -> pftreestate -> pftreestate
 val solve_nth_pftreestate : int -> tactic -> pftreestate -> pftreestate
 val solve_pftreestate : tactic -> pftreestate -> pftreestate
+
 (* a weak version of logical undoing, that is really correct only *)
 (* if there are no existential variables.                         *)
 val weak_undo_pftreestate : pftreestate -> pftreestate
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index 5a69ecf577..c0254a7ca6 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -150,6 +150,8 @@ let prev_unproven           = prev_unproven
 let top_of_tree             = top_of_tree
 let frontier                = frontier
 let change_constraints_pftreestate = change_constraints_pftreestate
+let instantiate_pf     = instantiate_pf
+let instantiate_pf_com = instantiate_pf_com
 
 (***********************************)
 (* Walking constraints re-exported *)
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index 0baa909c99..afb9016ea5 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -107,6 +107,8 @@ val prev_unproven           : pftreestate -> pftreestate
 val top_of_tree             : pftreestate -> pftreestate
 val change_constraints_pftreestate :
   global_constraints -> pftreestate -> pftreestate
+val instantiate_pf     : int -> constr -> pftreestate -> pftreestate
+val instantiate_pf_com : int -> Coqast.t -> pftreestate -> pftreestate
 
 
 (*s Tacticals re-exported from the Refiner module. *)
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 98a732287e..f27bf381b0 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -88,8 +88,7 @@ let mutual_fix   = Tacmach.mutual_fix
 let fix f n      = mutual_fix [f] [n] []
 
 let fix_noname n =  
-  let l = Pfedit.list_proofs() in
-  let id = id_of_string (List.hd l) in  
+  let id = id_of_string (Pfedit.get_current_proof_name ()) in
   fix id n
 
 let dyn_mutual_fix argsl gl = 
@@ -111,8 +110,7 @@ let mutual_cofix = Tacmach.mutual_cofix
 let cofix f      =  mutual_cofix [f] []
 
 let cofix_noname n =  
-  let l = Pfedit.list_proofs() in
-  let id = id_of_string (List.hd l) in  
+  let id = id_of_string (Pfedit.get_current_proof_name ()) in
   cofix id n
 
 let dyn_mutual_cofix argsl gl = 
@@ -1464,39 +1462,6 @@ let dImp cls gl =
     | None    -> intro gl
     | Some id -> impE id gl
 
-(******************************************)
-(* Instantiation of existential variables *)
-(******************************************)
-
-let instantiate_pf n c pfts = 
-  let gls = top_goal_of_pftreestate pfts in
-  let (wc,_) = startWalk gls in
-  let sigma  = (w_Underlying wc) in 
-  let (sp,_) = 
-    try 
-      List.nth (Evd.non_instantiated sigma) (n-1)
-    with Failure _ -> 
-      error "not so many uninstantiated existential variables"
-  in 
-  let wc' = w_Define sp c wc in 
-  let newgc = ts_mk (w_Underlying wc') in 
-  change_constraints_pftreestate newgc pfts
-
-let instantiate_pf_com n com pfts = 
-  let gls = top_goal_of_pftreestate pfts in
-  let (wc,_) = startWalk gls in
-  let sigma = (w_Underlying wc) in 
-  let (sp,evd) = 
-    try
-      List.nth (Evd.non_instantiated sigma) (n-1) 
-    with Failure _ -> 
-      error "not so many uninstantiated existential variables"
-  in 
-  let c = Astterm.interp_constr sigma evd.evar_env com in     
-  let wc' = w_Define sp c wc in
-  let newgc = ts_mk (w_Underlying wc') in
-  change_constraints_pftreestate newgc pfts
-
 (************************************************)
 (*  Tactics related with logic connectives      *)
 (************************************************)
@@ -1652,21 +1617,15 @@ let abstract_subproof name tac gls =
   let concl = Sign.it_sign (fun t id typ -> mkNamedProd id typ t)
                 (pf_concl gls) sign in
   let env' = change_hyps (fun _ -> current_sign) env in
-  let top_goal = mk_goal (mt_ctxt Intset.empty) env' concl in
-  let ts = { top_hyps = (Global.env(), empty_env);
-             top_goal = top_goal;
-             top_strength = Declare.NeverDischarge } 
-  in 
-  start(nas,ts);set_proof (Some nas);
+  start_proof nas Declare.NeverDischarge env' concl;
   begin 
     try
-      by (tclCOMPLETE (tclTHEN (tclDO (sign_length sign) intro) 
-			 tac)); 
+      by (tclCOMPLETE (tclTHEN (tclDO (sign_length sign) intro) tac)); 
       save_named true
     with e when catchable_exception e -> 
-      (abort_cur_goal(); raise e)
+      (abort_current_goal(); raise e)
   end;
-  exact (applist ((Declare.construct_reference env' CCI na), 
+  exact (applist ((Declare.construct_reference env' CCI na),
                   (List.map (fun id -> VAR(id)) 
                      (List.rev (ids_of_sign sign)))))
     gls
@@ -1674,7 +1633,7 @@ let abstract_subproof name tac gls =
 let tclABSTRACT name_op tac gls = 
   let s = match name_op with 
     | Some s -> s 
-    | None   -> id_of_string ((get_proof ())^"_subproof") 
+    | None   -> id_of_string ((get_current_proof_name ())^"_subproof") 
   in  
   abstract_subproof s tac gls
 
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 6ee8b95481..0f45a1e7cb 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -149,11 +149,6 @@ val dyn_apply             : tactic_arg list -> tactic
 val cut_and_apply         : constr -> tactic
 val dyn_cut_and_apply     : tactic_arg list -> tactic
 
-(*s Instantiation tactics. *)
-
-val instantiate_pf     : int -> constr -> pftreestate -> pftreestate
-val instantiate_pf_com : int -> Coqast.t -> pftreestate -> pftreestate
-
 (*s Elimination tactics. *)
 
 val general_elim   : constr * constr substitution ->
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 2f755b4e37..93426fde9b 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -372,3 +372,11 @@ let build_scheme lnamedepindsort =
   declare 0 lrecnames; 
   if is_verbose() then pPNL(recursive_message lrecnames)
 
+let start_proof_com s stre com =
+  let env = Global.env () in
+  Pfedit.start_proof s stre env (interp_type Evd.empty env com)
+
+let get_current_context () =
+  try Pfedit.get_current_goal_context ()
+  with e when Logic.catchable_exception e -> 
+    (Evd.empty, Global.env())
diff --git a/toplevel/command.mli b/toplevel/command.mli
index cd4cb930d5..1cc9d5a754 100644
--- a/toplevel/command.mli
+++ b/toplevel/command.mli
@@ -38,3 +38,4 @@ val build_corecursive :  (identifier * Coqast.t * Coqast.t) list -> unit
 
 val build_scheme : (identifier * bool * identifier * Coqast.t) list -> unit
 
+val start_proof_com : string -> strength -> Coqast.t -> unit
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index 8b1fc69f3f..079ad7ed16 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -310,7 +310,7 @@ let explain_refiner_cannot_unify m n =
      'sTR"with"; 'bRK(1,1) ; pn >]
 
 let explain_refiner_cannot_generalize ty =
-  [< 'sTR "cannot find a generalisation of the goal with type : "; 
+  [< 'sTR "Cannot find a well-typed generalisation of the goal with type : "; 
      prterm ty >]
 
 let explain_refiner_not_well_typed c =
diff --git a/toplevel/toplevel.ml b/toplevel/toplevel.ml
index 6d2ebf57ac..fcc7da2c2c 100644
--- a/toplevel/toplevel.ml
+++ b/toplevel/toplevel.ml
@@ -162,10 +162,13 @@ let valid_buffer_loc ib dloc (b,e) =
 (* A buffer to store the current command read on stdin. It is
  * initialized when a vernac command is immediately followed by "\n",
  * or after a Drop. *)
+let make_prompt () =
+  if Pfedit.refining () then
+    (Pfedit.get_current_proof_name ())^" < "
+  else "Coq < "
 
 let top_buffer =
-  let pr() = 
-    (Pfedit.proof_prompt())^(emacs_str (String.make 1 (Char.chr 249)))
+  let pr() = (make_prompt())^(emacs_str (String.make 1 (Char.chr 249)))
   in
   { prompt = pr;
     str = "";
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index e3adda7f0d..bad51033bf 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -125,9 +125,7 @@ and raw_compile_module verbosely only_spec mname file =
   Library.open_module mname;
   let lfname = read_vernac_file verbosely file in
   let base = Filename.chop_suffix lfname ".v" in
-  if Pfedit.refining () then
-    errorlabstrm "Vernac.raw_compile_module"
-      [< 'sTR"proof editing in progress" ; (Pfedit.msg_proofs false) >];
+  Pfedit.check_no_pending_proofs ();
   if only_spec then
     failwith ".vi not yet implemented"
   else 
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 1a45b8540b..f21768913e 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -101,11 +101,6 @@ let show_top_evars () =
   let sigma = project gls in 
   mSG (pr_evars_int 1 (Evd.non_instantiated sigma))
 
-(* Focus commands *)
-let reset_top_of_tree () = 
-  let pts = get_pftreestate () in 
-  if not (is_top_pftreestate pts) then Pfedit.mutate top_of_tree
-
 (* Locate commands *)
  
 let locate_file f =
@@ -125,9 +120,9 @@ let print_loadpath () =
   mSGNL [< 'sTR"Load Path:"; 'fNL; 'sTR"  ";
            hV 0 (prlist_with_sep pr_fnl (fun s -> [< 'sTR s >]) l) >]
 
-let goal_of_args = function
-  | [VARG_NUMBER n] -> Some n
-  | [] -> None
+let get_goal_context_of_args = function
+  | [VARG_NUMBER n] -> get_goal_context n
+  | [] -> get_current_goal_context ()
   | _ -> bad_vernac_args "goal_of_args"
 
 let isfinite = function 
@@ -218,24 +213,29 @@ let _ =
 
 (* Managing states *)
 
+let abort_refine f x =
+  if Pfedit.refining() then abort_goals ();
+  f x
+  (* used to be: error "Must save or abort current goal first" *)
+
 let _ =
   add "WriteState"
     (function 
        | [VARG_STRING file] ->
-	   (fun () -> Pfedit.abort_refine States.extern_state file)
+	   (fun () -> abort_refine States.extern_state file)
        | [VARG_IDENTIFIER id] ->
 	   let file = string_of_id id in
-	   (fun () -> Pfedit.abort_refine States.extern_state file)
+	   (fun () -> abort_refine States.extern_state file)
        | _ -> bad_vernac_args "SaveState")
 
 let _ =
   add "RestoreState"
     (function 
        | [VARG_STRING file] ->
-	   (fun () -> Pfedit.abort_refine States.intern_state file)
+	   (fun () -> abort_refine States.intern_state file)
        | [VARG_IDENTIFIER id] ->
 	   let file = string_of_id id in
-	   (fun () -> Pfedit.abort_refine States.intern_state file)
+	   (fun () -> abort_refine States.intern_state file)
        | _ -> bad_vernac_args "LoadState")
 
 (* Resetting *)
@@ -244,13 +244,13 @@ let _ =
   add "ResetName"
     (function 
        | [VARG_IDENTIFIER id] -> 
-	   (fun () -> Pfedit.abort_refine Lib.reset_name id)
+	   (fun () -> abort_refine Lib.reset_name id)
        | _ -> bad_vernac_args "ResetName")
 
 let _ =
   add "ResetInitial"
     (function 
-       | [] -> (fun () -> Pfedit.abort_refine Lib.reset_initial ())
+       | [] -> (fun () -> abort_refine Lib.reset_initial ())
        | _  -> bad_vernac_args "ResetInitial")
 
 (***
@@ -328,10 +328,7 @@ let _ =
     (function 
        | [VARG_IDENTIFIER id] ->
 	   (fun () ->
-              if refining () then 
-		errorlabstrm "vernacentries : EndSection"
-		  [< 'sTR"proof editing in progress" ; (msg_proofs false) ;
-                     'sTR"Use \"Abort All\" first or complete proof(s)." >];
+	      check_no_pending_proofs ();
               Discharge.close_section (not (is_silent())) (string_of_id id))
        | _ -> bad_vernac_args "EndSection")
 
@@ -343,7 +340,7 @@ let _ =
        | [VARG_CONSTR com] ->
 	   (fun () ->
               if not (refining()) then begin
-              	start_proof "Unnamed_thm" NeverDischarge com;
+              	start_proof_com "Unnamed_thm" NeverDischarge com;
 		if not (is_silent()) then show_open_subgoals ()
               end else 
 		error "repeated Goal not permitted in refining mode")
@@ -357,13 +354,21 @@ let _ =
 	   (fun () -> 
 	      let s = string_of_id id in
 	      abort_goal s; message ("Goal "^s^" aborted"))
-       | [] -> (fun () -> abort_cur_goal (); message "Current goal aborted")
+       | [] -> (fun () -> 
+		  abort_current_goal ();
+		  message "Current goal aborted")
        | _  -> bad_vernac_args "ABORT")
 
 let _ =
   add "ABORTALL"
     (function 
-       | [] -> (fun () -> abort_goals())
+       | [] -> (fun () ->
+		  if refining() then begin
+		    abort_goals ();
+		    message "Current goals aborted"
+		  end else
+		    error "No proof-editing in progress")
+
        | _  -> bad_vernac_args "ABORTALL")
 
 let _ =
@@ -375,15 +380,15 @@ let _ =
 let _ =
   add "SUSPEND"
     (function 
-       | [] -> (fun () -> set_proof None)
+       | [] -> (fun () -> set_current_proof None)
        | _  -> bad_vernac_args "SUSPEND")
 
 let _ =
   add "RESUME"
     (function 
        | [VARG_IDENTIFIER id] ->
-	   (fun () -> set_proof (Some(string_of_id id)))
-       | [] -> (fun () -> resume_last ())
+	   (fun () -> set_current_proof (Some(string_of_id id)))
+       | [] -> (fun () -> resume_last_proof ())
        | _  -> bad_vernac_args "RESUME")
 
 let _ =
@@ -509,11 +514,11 @@ let _ =
        | [VARG_NUMBER n] ->
 	   (fun () -> (Pfedit.traverse n;show_node()))
        | [VARG_STRING"top"] ->
-           (fun () -> (mutate top_of_tree;show_node()))
+           (fun () -> (Pfedit.reset_top_of_tree ();show_node()))
        | [VARG_STRING"next"] ->
-           (fun () -> (mutate next_unproven;show_node()))
+           (fun () -> (Pfedit.traverse_next_unproven ();show_node()))
        | [VARG_STRING"prev"] ->
-           (fun () -> (mutate prev_unproven;show_node()))
+           (fun () -> (Pfedit.traverse_prev_unproven ();show_node()))
        | _ -> bad_vernac_args "Go")
 
 let _ =
@@ -608,7 +613,7 @@ let _ =
   add "ShowProofs"
     (function [] ->
        (fun () ->
-	  let l = Pfedit.list_proofs() in 
+	  let l = Pfedit.get_all_proof_names() in 
 	  mSGNL (prlist_with_sep pr_spc pr_str l))
        | _  -> bad_vernac_args "ShowProofs")
 
@@ -660,7 +665,7 @@ let _ =
 let _ =
   add "StartProof"
     (function 
-       | [VARG_STRING kind;VARG_IDENTIFIER s;VARG_CONSTR c] ->
+       | [VARG_STRING kind;VARG_IDENTIFIER s;VARG_CONSTR com] ->
 	   let stre = match kind with
 	     | "THEOREM" -> NeverDischarge
              | "LEMMA" -> NeverDischarge
@@ -673,7 +678,7 @@ let _ =
            in 
 	   fun () ->
              begin
-               start_proof (string_of_id s) stre c;
+               start_proof_com (string_of_id s) stre com;
                if (not(is_silent())) then show_open_subgoals()
              end
        | _ -> bad_vernac_args "StartProof")
@@ -682,7 +687,7 @@ let _ =
   add "TheoremProof"
     (function 
        | [VARG_STRING kind; VARG_IDENTIFIER s; 
-	  VARG_CONSTR c; VARG_VARGLIST coml] ->
+	  VARG_CONSTR com; VARG_VARGLIST coml] ->
 	   let calls = List.map
 			 (function 
 			    | (VCALL(na,l)) -> (na,l)
@@ -703,7 +708,7 @@ let _ =
               try
             	States.with_heavy_rollback
 		  (fun () ->
-                     start_proof (string_of_id s) stre c;
+                     start_proof_com (string_of_id s) stre com;
                      if not (is_silent()) then show_open_subgoals();
                      List.iter Vernacinterp.call calls;
                      if not (is_silent()) then show_script();
@@ -714,8 +719,8 @@ let _ =
                   mSGNL [< 'sTR"Error: checking of theorem " ; print_id s ;
                            'sPC ; 'sTR"failed" ;
                            'sTR"... converting to Axiom" >];
-                  del_proof (string_of_id s);
-                  parameter_def_var (string_of_id s) c
+                  abort_goal (string_of_id s);
+                  parameter_def_var (string_of_id s) com
            	end else 
 		  errorlabstrm "vernacentries__TheoremProof"
                     [< 'sTR"checking of theorem " ; print_id s ; 'sPC ;
@@ -809,7 +814,7 @@ let _ =
   add "Eval"
     (function
        | VARG_TACTIC_ARG (Redexp redexp) :: VARG_CONSTR c :: g ->
-           let (evmap,sign) = get_evmap_sign (goal_of_args g) in
+           let (evmap,sign) = get_goal_context_of_args g in
            let redfun = print_eval (reduction_of_redexp redexp) sign in 
 	   fun () -> mSG (redfun (judgment_of_com evmap sign c))
        | _ -> bad_vernac_args "Eval")
@@ -818,7 +823,7 @@ let _ =
   add "Check"
     (function 
        | VARG_STRING kind :: VARG_CONSTR c :: g ->
-	   let (evmap, sign) = get_evmap_sign (goal_of_args g) in
+	   let (evmap, sign) = get_goal_context_of_args g in
 	   let prfun = match kind with
 	     | "CHECK" -> print_val
              | "PRINTTYPE" -> print_type
@@ -862,7 +867,7 @@ let _ =
 let _ =
   add "UNSETUNDO"
     (function 
-       | [] -> (fun () -> unset_undo ())
+       | [] -> (fun () -> reset_undo ())
        | _  -> bad_vernac_args "UNSETUNDO")
 
 let _ =
@@ -1407,7 +1412,7 @@ let _ =
   vinterp_add "EXISTENTIAL"
     (function 
        | [VARG_NUMBER n; VARG_CONSTR c] -> 
-           (fun () -> mutate (instantiate_pf_com n c))
+           (fun () -> instantiate_nth_evar_com n c)
        |  _  -> assert false)
 
 (* The second is a stupid macro that should be replaced by ``Exact
@@ -1449,5 +1454,5 @@ let _ =
           (* in case a strict subtree was completed, 
               go back to the top of the prooftree *) 
 	  if subtree_solved () then 
-	    (rev_mutate top_of_tree; print_subgoals()) 
+	    (reset_top_of_tree (); print_subgoals()) 
        ))
diff --git a/toplevel/vernacinterp.ml b/toplevel/vernacinterp.ml
index ea27b4aa67..1f55e4a3ec 100644
--- a/toplevel/vernacinterp.ml
+++ b/toplevel/vernacinterp.ml
@@ -96,9 +96,8 @@ let rec cvt_varg ast =
     | Node(_,"AST",[a]) -> VARG_AST a
     | Node(_,"ASTLIST",al) -> VARG_ASTLIST al
     | Node(_,"TACTIC_ARG",[targ]) ->
-      let (evc,env)=Pfedit.get_evmap_sign None
-      in
-        VARG_TACTIC_ARG (interp_tacarg (evc,env,[],[],None) targ)
+      let (evc,env)= Pfedit.get_current_goal_context () in
+      VARG_TACTIC_ARG (interp_tacarg (evc,env,[],[],None) targ)
     | Node(_,"VERNACDYN",[Dynamic (_,d)]) -> VARG_DYN d
     | _ -> anomaly_loc (Ast.loc ast, "Vernacinterp.cvt_varg",
                         [< 'sTR "Unrecognizable ast node of vernac arg:";