Imported Upstream version 8.5~beta1+dfsg

1 files changed, 450 insertions, 212 deletions

diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index a58fab0c..f55ab700 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -14,6 +14,7 @@
 (*                                                                     *)
 (***********************************************************************)
 
+open Util
 open Pp
 open Names
 
@@ -32,15 +33,17 @@ let proof_modes = Hashtbl.create 6
 let find_proof_mode n =
   try Hashtbl.find proof_modes n
   with Not_found ->
-    Util.error (Format.sprintf "No proof mode named \"%s\"." n)
+    Errors.error (Format.sprintf "No proof mode named \"%s\"." n)
+
+let register_proof_mode ({name = n} as m) =
+  Hashtbl.add proof_modes n (Ephemeron.create m)
 
-let register_proof_mode ({ name = n } as m) = Hashtbl.add proof_modes n m
 (* initial mode: standard mode *)
 let standard = { name = "No" ; set = (fun ()->()) ; reset = (fun () -> ()) }
 let _ = register_proof_mode standard
 
 (* Default proof mode, to be set at the beginning of proofs. *)
-let default_proof_mode = ref standard
+let default_proof_mode = ref (find_proof_mode "No")
 
 let _ =
   Goptions.declare_string_option {Goptions.
@@ -48,48 +51,63 @@ let _ =
     optdepr = false;
     optname = "default proof mode" ;
     optkey = ["Default";"Proof";"Mode"] ;
-    optread = begin fun () -> 
-                               let { name = name } = !default_proof_mode in name 
-                     end;
-    optwrite = begin fun n -> 
-                                default_proof_mode := find_proof_mode n
-                      end
+    optread = begin fun () ->
+      (Ephemeron.default !default_proof_mode standard).name
+    end;
+    optwrite = begin fun n ->
+      default_proof_mode := find_proof_mode n
+    end
   }
 
 (*** Proof Global Environment ***)
 
-(* local shorthand *)
-type nproof = identifier*Proof.proof
-
 (* Extra info on proofs. *)
 type lemma_possible_guards = int list list
-type proof_info = { 
-  strength : Decl_kinds.goal_kind ;
-  compute_guard :  lemma_possible_guards; 
-  hook :Tacexpr.declaration_hook ;
-  mode : proof_mode
+type proof_universes = Evd.evar_universe_context
+
+type proof_object = {
+  id : Names.Id.t;
+  entries : Entries.definition_entry list;
+  persistence : Decl_kinds.goal_kind;
+  universes: proof_universes;
+  (* constraints : Univ.constraints; *)
+}
+
+type proof_ending =
+  | Admitted
+  | Proved of Vernacexpr.opacity_flag *
+             (Vernacexpr.lident * Decl_kinds.theorem_kind option) option *
+              proof_object
+type proof_terminator = proof_ending -> unit
+type closed_proof = proof_object * proof_terminator
+
+type pstate = {
+  pid : Id.t;
+  terminator : proof_terminator Ephemeron.key;
+  endline_tactic : Tacexpr.raw_tactic_expr option;
+  section_vars : Context.section_context option;
+  proof : Proof.proof;
+  strength : Decl_kinds.goal_kind;
+  mode : proof_mode Ephemeron.key;
 }
 
-(* Invariant: the domain of proof_info is current_proof.*)
-(* The head of [!current_proof] is the actual current proof, the other ones are
+(* The head of [!pstates] is the actual current proof, the other ones are
    to be resumed when the current proof is closed or aborted. *)
-let current_proof = ref ([]:nproof list)
-let proof_info = ref (Idmap.empty : proof_info Idmap.t)
+let pstates = ref ([] : pstate list)
 
 (* Current proof_mode, for bookkeeping *)
 let current_proof_mode = ref !default_proof_mode
 
 (* combinators for proof modes *)
-let update_proof_mode () = 
-  match !current_proof with
-  | (id,_)::_ ->  
-      let { mode = m } = Idmap.find id !proof_info in
-      !current_proof_mode.reset ();
+let update_proof_mode () =
+  match !pstates with
+  | { mode = m } :: _ ->
+      Ephemeron.iter_opt !current_proof_mode (fun x -> x.reset ());
       current_proof_mode := m;
-      !current_proof_mode.set ()
-  | _ -> 
-      !current_proof_mode.reset (); 
-      current_proof_mode := standard
+      Ephemeron.iter_opt !current_proof_mode (fun x -> x.set ())
+  | _ ->
+      Ephemeron.iter_opt !current_proof_mode (fun x -> x.reset ());
+      current_proof_mode := find_proof_mode "No"
 
 (* combinators for the current_proof lists *)
 let push a l = l := a::!l;
@@ -97,213 +115,271 @@ let push a l = l := a::!l;
 
 exception NoSuchProof
 let _ = Errors.register_handler begin function
-  | NoSuchProof -> Util.error "No such proof."
+  | NoSuchProof -> Errors.error "No such proof."
   | _ -> raise Errors.Unhandled
 end
-let rec extract id l = 
-  let rec aux = function
-    | ((id',_) as np)::l when id_ord id id' = 0 -> (np,l)
-    | np::l -> let (np', l) = aux l in (np' , np::l)
-    | [] -> raise NoSuchProof
-  in
-  let (np,l') = aux !l in
-  l := l';
-  update_proof_mode ();
-  np
 
 exception NoCurrentProof
 let _ = Errors.register_handler begin function
-  | NoCurrentProof -> Util.error "No focused proof (No proof-editing in progress)."
+  | NoCurrentProof -> Errors.error "No focused proof (No proof-editing in progress)."
   | _ -> raise Errors.Unhandled
 end
-let extract_top l =
-  match !l with
-  | np::l' -> l := l' ; update_proof_mode (); np
-  | [] -> raise NoCurrentProof	
-let find_top l =
-  match !l with
+
+(*** Proof Global manipulation ***)
+
+let get_all_proof_names () =
+  List.map (function { pid = id } -> id) !pstates
+
+let cur_pstate () =
+  match !pstates with
   | np::_ -> np
   | [] -> raise NoCurrentProof
 
-let rotate_top l1 l2 =
-  let np = extract_top l1 in
-  push np l2
+let give_me_the_proof () = (cur_pstate ()).proof
+let get_current_proof_name () = (cur_pstate ()).pid
 
-let rotate_find id l1 l2 =
-  let np = extract id l1 in
-  push np l2
-  
+let interp_tac = ref (fun _ -> assert false)
+let set_interp_tac f = interp_tac := f
 
-(* combinators for the proof_info map *)
-let add id info m =
-  m := Idmap.add id info !m
-let remove id m =
-  m := Idmap.remove id !m
-
-(*** Proof Global manipulation ***)
+let with_current_proof f =
+  match !pstates with
+  | [] -> raise NoCurrentProof
+  | p :: rest ->
+      let et =
+        match p.endline_tactic with
+        | None -> Proofview.tclUNIT ()
+        | Some tac -> !interp_tac tac in
+      let (newpr,ret) = f et p.proof in
+      let p = { p with proof = newpr } in
+      pstates := p :: rest;
+      ret
+let simple_with_current_proof f = with_current_proof (fun t p -> f t p , ())
 
-let get_all_proof_names () =
-    List.map fst !current_proof
+let compact_the_proof () = simple_with_current_proof (fun _ -> Proof.compact)
 
-let give_me_the_proof () = 
-  snd (find_top current_proof)
 
-let get_current_proof_name () =
-  fst (find_top current_proof)
+(* Sets the tactic to be used when a tactic line is closed with [...] *)
+let set_endline_tactic tac =
+  match !pstates with
+  | [] -> raise NoCurrentProof
+  | p :: rest -> pstates := { p with endline_tactic = Some tac } :: rest
 
 (* spiwack: it might be considered to move error messages away.
     Or else to remove special exceptions from Proof_global.
     Arguments for the former: there is no reason Proof_global is only
-    accessed directly through vernacular commands. Error message should be 
+    accessed directly through vernacular commands. Error message should be
    pushed to external layers, and so we should be able to have a finer
    control on error message on complex actions. *)
 let msg_proofs () =
   match get_all_proof_names () with
     | [] -> (spc () ++ str"(No proof-editing in progress).")
     | l ->  (str"." ++ fnl () ++ str"Proofs currently edited:" ++ spc () ++
-               (Util.prlist_with_sep Util.pr_spc Nameops.pr_id l)++ str ".")
+               (pr_sequence Nameops.pr_id l) ++ str".")
 
-let there_is_a_proof () = !current_proof <> []
+let there_is_a_proof () = not (List.is_empty !pstates)
 let there_are_pending_proofs () = there_is_a_proof ()
 let check_no_pending_proof () =
   if not (there_are_pending_proofs ()) then
     ()
   else begin
-    Util.error (Pp.string_of_ppcmds
+    Errors.error (Pp.string_of_ppcmds
       (str"Proof editing in progress" ++ msg_proofs () ++ fnl() ++
        str"Use \"Abort All\" first or complete proof(s)."))
   end
 
 let discard_gen id =
-  ignore (extract id current_proof);
-  remove id proof_info
-
-let discard (loc,id) = 
-  try
-    discard_gen id
-  with NoSuchProof ->
-    Util.user_err_loc
+  pstates := List.filter (fun { pid = id' } -> not (Id.equal id id')) !pstates
+
+let discard (loc,id) =
+  let n = List.length !pstates in
+  discard_gen id;
+  if Int.equal (List.length !pstates) n then
+    Errors.user_err_loc
       (loc,"Pfedit.delete_proof",str"No such proof" ++ msg_proofs ())
 
 let discard_current () =
-  let (id,_) = extract_top current_proof in
-  remove id proof_info
- 
-let discard_all () =
-  current_proof := [];
-  proof_info := Idmap.empty
+  if List.is_empty !pstates then raise NoCurrentProof else pstates := List.tl !pstates
+
+let discard_all () = pstates := []
 
 (* [set_proof_mode] sets the proof mode to be used after it's called. It is
     typically called by the Proof Mode command. *)
-(* Core component.
-    No undo handling.
-    Applies to proof [id], and proof mode [m]. *)
-let set_proof_mode m id = 
-  let info = Idmap.find id !proof_info in
-  let info = { info with mode = m } in
-  proof_info := Idmap.add id info !proof_info;
+let set_proof_mode m id =
+  pstates :=
+    List.map (function { pid = id' } as p ->
+      if Id.equal id' id then { p with mode = m } else p) !pstates;
   update_proof_mode ()
-(* Complete function.
-    Handles undo.
-    Applies to current proof, and proof mode name [mn]. *)
-let set_proof_mode mn =
-  let m = find_proof_mode mn in
-  let id = get_current_proof_name () in
-  let pr = give_me_the_proof () in
-  Proof.add_undo begin let curr = !current_proof_mode in fun () ->
-    set_proof_mode curr id ; update_proof_mode ()
-  end pr ;
-  set_proof_mode m id
-
-exception AlreadyExists
-let _ = Errors.register_handler begin function
-  | AlreadyExists -> Util.error "Already editing something of that name."
-  | _ -> raise Errors.Unhandled
-end
-(* [start_proof s str env t hook tac] starts a proof of name [s] and
-    conclusion [t]; [hook] is optionally a function to be applied at
-    proof end (e.g. to declare the built constructions as a coercion
-    or a setoid morphism); init_tac is possibly a tactic to
-    systematically apply at initialization time (e.g. to start the
-    proof of mutually dependent theorems).
-    It raises exception [ProofInProgress] if there is a proof being
-    currently edited. *)
-let start_proof  id str goals ?(compute_guard=[]) hook =
-  begin
-    List.iter begin fun (id_ex,_) ->
-      if Names.id_ord id id_ex = 0 then raise AlreadyExists
-    end !current_proof
-  end;
-  let p = Proof.start goals in
-  add id { strength=str ; 
-	        compute_guard=compute_guard ; 
-		hook=hook ;
-	        mode = ! default_proof_mode } proof_info ;
-  push (id,p) current_proof
-
-(* arnaud: à enlever *)
-let run_tactic tac = 
-  let p = give_me_the_proof () in
-  let env = Global.env () in
-  Proof.run_tactic env tac p
 
-(* Sets the tactic to be used when a tactic line is closed with [...] *)
-let set_endline_tactic tac =
-  let p = give_me_the_proof () in
-  Proof.set_endline_tactic tac p
+let set_proof_mode mn =
+  set_proof_mode (find_proof_mode mn) (get_current_proof_name ())
+
+let activate_proof_mode mode =
+  Ephemeron.iter_opt (find_proof_mode mode) (fun x -> x.set ())
+let disactivate_proof_mode mode =
+  Ephemeron.iter_opt (find_proof_mode mode) (fun x -> x.reset ())
+
+(** [start_proof sigma id str goals terminator] starts a proof of name
+    [id] with goals [goals] (a list of pairs of environment and
+    conclusion); [str] describes what kind of theorem/definition this
+    is (spiwack: for potential printing, I believe is used only by
+    closing commands and the xml plugin); [terminator] is used at the
+    end of the proof to close the proof. The proof is started in the
+    evar map [sigma] (which can typically contain universe
+    constraints). *)
+let start_proof sigma id str goals terminator =
+  let initial_state = {
+    pid = id;
+    terminator = Ephemeron.create terminator;
+    proof = Proof.start sigma goals;
+    endline_tactic = None;
+    section_vars = None;
+    strength = str;
+    mode = find_proof_mode "No" } in
+  push initial_state pstates
+
+let start_dependent_proof id str goals terminator =
+  let initial_state = {
+    pid = id;
+    terminator = Ephemeron.create terminator;
+    proof = Proof.dependent_start goals;
+    endline_tactic = None;
+    section_vars = None;
+    strength = str;
+    mode = find_proof_mode "No" } in
+  push initial_state pstates
+
+let get_used_variables () = (cur_pstate ()).section_vars
 
 let set_used_variables l =
-  let p = give_me_the_proof () in
   let env = Global.env () in
-  let ids = List.fold_right Idset.add l Idset.empty in
+  let ids = List.fold_right Id.Set.add l Id.Set.empty in
   let ctx = Environ.keep_hyps env ids in
-  Proof.set_used_variables ctx p
-
-let get_used_variables () =
-  Proof.get_used_variables (give_me_the_proof ())
-
-let with_end_tac tac =
-  let p = give_me_the_proof () in
-  Proof.with_end_tac p tac
-
-let close_proof () =
-  (* spiwack: for now close_proof doesn't actually discard the proof, it is done
-      by [Command.save]. *)
-  try 
-    let id = get_current_proof_name () in
-    let p = give_me_the_proof () in
-    let proofs_and_types = Proof.return p in
-    let section_vars = Proof.get_used_variables p in
-    let entries = List.map
-      (fun (c,t) -> { Entries.const_entry_body = c;
-                      const_entry_secctx = section_vars;
-                      const_entry_type = Some t;
-		      const_entry_opaque = true })
-      proofs_and_types
-    in
-    let { compute_guard=cg ; strength=str ; hook=hook } =
-      Idmap.find id !proof_info
-    in
-    (id, (entries,cg,str,hook))
-  with 
-    |  Proof.UnfinishedProof ->
-	 Util.error "Attempt to save an incomplete proof"
-    | Proof.HasUnresolvedEvar ->
-	Util.error "Attempt to save a proof with existential variables still non-instantiated"
-
+  match !pstates with
+  | [] -> raise NoCurrentProof
+  | p :: rest ->
+      if not (Option.is_empty p.section_vars) then
+        Errors.error "Used section variables can be declared only once";
+      pstates := { p with section_vars = Some ctx} :: rest;
+      ctx
+
+let get_open_goals () =
+  let gl, gll, shelf , _ , _ = Proof.proof (cur_pstate ()).proof in
+  List.length gl +
+    List.fold_left (+) 0
+    (List.map (fun (l1,l2) -> List.length l1 + List.length l2) gll) +
+    List.length shelf
+
+let close_proof ~keep_body_ucst_sepatate ?feedback_id ~now fpl =
+  let { pid; section_vars; strength; proof; terminator } = cur_pstate () in
+  let poly = pi2 strength (* Polymorphic *) in
+  let initial_goals = Proof.initial_goals proof in
+  let fpl, univs = Future.split2 fpl in
+  let universes = 
+    if poly || now then Future.force univs 
+    else Proof.in_proof proof (fun x -> Evd.evar_universe_context x) 
+  in
+  (* Because of dependent subgoals at the begining of proofs, we could
+     have existential variables in the initial types of goals, we need to
+     normalise them for the kernel. *)
+  let subst_evar k =
+    Proof.in_proof proof (fun m -> Evd.existential_opt_value m k) in
+  let nf = Universes.nf_evars_and_universes_opt_subst subst_evar
+    (Evd.evar_universe_context_subst universes) in
+  let make_body =
+    if poly || now then
+      let make_body t (c, eff) =
+        let open Universes in
+	let body = c and typ = nf t in
+        let used_univs_body = Universes.universes_of_constr body in
+	let used_univs_typ = Universes.universes_of_constr typ in
+	let ctx = Evd.evar_universe_context_set universes in
+        if keep_body_ucst_sepatate then
+          (* For vi2vo compilation proofs are computed now but we need to
+           * completent the univ constraints of the typ with the ones of
+           * the body.  So we keep the two sets distinct. *)
+          let ctx_body = restrict_universe_context ctx used_univs_body in
+          let ctx_typ = restrict_universe_context ctx used_univs_typ in
+          let univs_typ = Univ.ContextSet.to_context ctx_typ in
+          (univs_typ, typ), ((body, ctx_body), eff)
+        else
+          (* Since the proof is computed now, we can simply have 1 set of
+           * constraints in which we merge the ones for the body and the ones
+           * for the typ *)
+          let used_univs = Univ.LSet.union used_univs_body used_univs_typ in
+          let ctx = restrict_universe_context ctx used_univs in
+          let univs = Univ.ContextSet.to_context ctx in
+          (univs, typ), ((body, Univ.ContextSet.empty), eff)
+      in 
+	fun t p ->
+	  Future.split2 (Future.chain ~pure:true p (make_body t))
+    else
+      fun t p ->
+        let initunivs = Evd.evar_context_universe_context universes in
+	  Future.from_val (initunivs, nf t), 
+	  Future.chain ~pure:true p (fun (pt,eff) ->
+	    (pt, Evd.evar_universe_context_set (Future.force univs)), eff)
+  in
+  let entries =
+    Future.map2 (fun p (_, t) ->
+      let univstyp, body = make_body t p in
+      let univs, typ = Future.force univstyp in
+	{ Entries.
+	  const_entry_body = body;
+	  const_entry_secctx = section_vars;
+	  const_entry_feedback = feedback_id;
+	  const_entry_type  = Some typ;
+	  const_entry_inline_code = false;
+	  const_entry_opaque = true;
+	  const_entry_universes = univs;
+	  const_entry_polymorphic = poly})
+      fpl initial_goals in
+  { id = pid; entries = entries; persistence = strength; universes = universes },
+  fun pr_ending -> Ephemeron.get terminator pr_ending
+
+type closed_proof_output = (Term.constr * Declareops.side_effects) list * Evd.evar_universe_context
+
+let return_proof () =
+  let { proof; strength = (_,poly,_) } = cur_pstate () in
+  let initial_goals = Proof.initial_goals proof in
+  let evd =
+    let error s = raise (Errors.UserError("last tactic before Qed",s)) in
+    try Proof.return proof with
+    | Proof.UnfinishedProof ->
+        error(str"Attempt to save an incomplete proof")
+    | Proof.HasShelvedGoals ->
+        error(str"Attempt to save a proof with shelved goals")
+    | Proof.HasGivenUpGoals ->
+        error(str"Attempt to save a proof with given up goals")
+    | Proof.HasUnresolvedEvar->
+        error(str"Attempt to save a proof with existential " ++
+              str"variables still non-instantiated") in
+  let eff = Evd.eval_side_effects evd in
+  let evd =
+    if poly || !Flags.compilation_mode = Flags.BuildVo
+    then Evd.nf_constraints evd
+    else evd in
+  (** ppedrot: FIXME, this is surely wrong. There is no reason to duplicate
+      side-effects... This may explain why one need to uniquize side-effects
+      thereafter... *)
+  let proofs = 
+    List.map (fun (c, _) -> (Evarutil.nf_evars_universes evd c, eff)) initial_goals in
+    proofs, Evd.evar_universe_context evd
+
+let close_future_proof ~feedback_id proof =
+  close_proof ~keep_body_ucst_sepatate:true ~feedback_id ~now:false proof
+let close_proof ~keep_body_ucst_sepatate fix_exn =
+  close_proof ~keep_body_ucst_sepatate ~now:true
+    (Future.from_val ~fix_exn (return_proof ()))
+
+(** Gets the current terminator without checking that the proof has
+    been completed. Useful for the likes of [Admitted]. *)
+let get_terminator () = Ephemeron.get ( cur_pstate() ).terminator
+let set_terminator hook =
+  match !pstates with
+  | [] -> raise NoCurrentProof
+  | p :: ps -> pstates := { p with terminator = Ephemeron.create hook } :: ps
 
-(**********************************************************)
-(*                                                                                                  *)
-(*                              Utility functions                                          *)
-(*                                                                                                  *)
-(**********************************************************)
 
-let maximal_unfocus k p =
-  begin try while Proof.no_focused_goal p do
-    Proof.unfocus k p
-  done
-  with Proof.FullyUnfocused | Proof.CannotUnfocusThisWay -> ()
-  end
 
 
 (**********************************************************)
@@ -314,14 +390,25 @@ let maximal_unfocus k p =
 
 module Bullet = struct
 
-  open Store.Field
+  type t = Vernacexpr.bullet
+
+  let bullet_eq b1 b2 = match b1, b2 with
+  | Vernacexpr.Dash n1, Vernacexpr.Dash n2 -> n1 = n2
+  | Vernacexpr.Star n1, Vernacexpr.Star n2 -> n1 = n2
+  | Vernacexpr.Plus n1, Vernacexpr.Plus n2 -> n1 = n2
+  | _ -> false
 
+  let pr_bullet b =
+    match b with
+    | Vernacexpr.Dash n -> str (String.make n '-')
+    | Vernacexpr.Star n -> str (String.make n '*')
+    | Vernacexpr.Plus n -> str (String.make n '+')
 
-  type t = Vernacexpr.bullet
 
   type behavior = {
     name : string;
-    put : Proof.proof -> t -> unit
+    put : Proof.proof -> t -> Proof.proof;
+    suggest: Proof.proof -> string option
   }
 
   let behaviors = Hashtbl.create 4
@@ -330,11 +417,55 @@ module Bullet = struct
   (*** initial modes ***)
   let none = {
     name = "None";
-    put = fun _ _ -> ()
+    put = (fun x _ -> x);
+    suggest = (fun _ -> None)
   }
   let _ = register_behavior none
 
   module Strict = struct
+    type suggestion =
+    | Suggest of t (* this bullet is mandatory here *)
+    | Unfinished of t (* no mandatory bullet here, but this bullet is unfinished *)
+    | NoBulletInUse (* No mandatory bullet (or brace) here, no bullet pending,
+		       some focused goals exists. *)
+    | NeedClosingBrace (* Some unfocussed goal exists "{" needed to focus them *)
+    | ProofFinished (* No more goal anywhere *)
+
+    (* give a message only if more informative than the standard coq message *)
+    let suggest_on_solved_goal sugg =
+      match sugg with
+      | NeedClosingBrace -> Some "Try unfocusing with \"}\"."
+      | NoBulletInUse -> None
+      | ProofFinished -> None
+      | Suggest b -> Some ("Focus next goal with bullet "
+			   ^ Pp.string_of_ppcmds (Pp.(pr_bullet b))
+			   ^".")
+      | Unfinished b -> Some ("The current bullet "
+			      ^ Pp.string_of_ppcmds (Pp.(pr_bullet b))
+			      ^ " is unfinished.")
+
+    (* give always a message. *)
+    let suggest_on_error sugg =
+      match sugg with
+      | NeedClosingBrace -> "Try unfocusing with \"}\"."
+      | NoBulletInUse -> assert false (* This should never raise an error. *)
+      | ProofFinished -> "No more subgoals."
+      | Suggest b -> ("Bullet " ^ Pp.string_of_ppcmds (Pp.(pr_bullet b))
+		      ^ " is mandatory here.")
+      | Unfinished b -> ("Current bullet " ^ Pp.string_of_ppcmds (Pp.(pr_bullet b))
+			 ^ " is not finished.")
+
+    exception FailedBullet of t * suggestion
+
+    let _ =
+      Errors.register_handler
+	(function
+	| FailedBullet (b,sugg) ->
+	  let prefix = "Wrong bullet " ^ Pp.string_of_ppcmds (Pp.(pr_bullet b)) ^ " : " in
+	  Errors.errorlabstrm "Focus" (str prefix ++ str (suggest_on_error sugg))
+	| _ -> raise Errors.Unhandled)
+
+
     (* spiwack: we need only one focus kind as we keep a stack of (distinct!) bullets *)
     let bullet_kind = (Proof.new_focus_kind () : t list Proof.focus_kind)
     let bullet_cond = Proof.done_cond ~loose_end:true bullet_kind
@@ -350,42 +481,88 @@ module Bullet = struct
 
     let has_bullet bul pr =
       let rec has_bullet = function
-	| b'::_ when bul=b' -> true
+	| b'::_ when bullet_eq bul b' -> true
 	| _::l -> has_bullet l
 	| [] -> false
       in
       has_bullet (get_bullets pr)
 
-    (* precondition: the stack is not empty *)
+    (* pop a bullet from proof [pr]. There should be at least one
+       bullet in use. If pop impossible (pending proofs on this level
+       of bullet or higher) then raise [Proof.CannotUnfocusThisWay]. *)
     let pop pr =
       match get_bullets pr with
-      | b::_ ->
-	Proof.unfocus bullet_kind pr;
-	(*returns*) b
+      | b::_ -> Proof.unfocus bullet_kind pr () , b
       | _ -> assert false
 
-    let push b pr =
+    let push (b:t) pr =
       Proof.focus bullet_cond (b::get_bullets pr) 1 pr
 
+    (* Used only in the next function.
+       TODO: use a recursive function instead? *)
+    exception SuggestFound of t
+
+    let suggest_bullet (prf:Proof.proof): suggestion =
+      if Proof.is_done prf then ProofFinished
+      else if not (Proof.no_focused_goal prf)
+      then (* No suggestion if a bullet is not mandatory, look for an unfinished bullet *)
+	match get_bullets prf with
+	| b::_ -> Unfinished b
+	| _ -> NoBulletInUse
+      else (* There is no goal under focus but some are unfocussed,
+	      let us look at the bullet needed. If no  *)
+	let pcobaye = ref prf in
+	try
+	  while true do
+	    let pcobaye', b = pop !pcobaye in
+	   (* pop went well, this means that there are no more goals
+	    *under this* bullet b, see if a new b can be pushed. *)
+	    (try let _ = push b pcobaye' in (* push didn't fail so a new b can be pushed. *)
+		 raise (SuggestFound b)
+	     with SuggestFound _ as e -> raise e
+	     | _ -> ()); (* b could not be pushed, so we must look for a outer bullet *)
+	    pcobaye := pcobaye'
+	  done;
+	  assert false
+	with SuggestFound b -> Suggest b
+	| _ -> NeedClosingBrace (* No push was possible, but there are still
+				   subgoals somewhere: there must be a "}" to use. *)
+
+
+    let rec pop_until (prf:Proof.proof) bul: Proof.proof =
+      let prf', b = pop prf in
+      if bullet_eq bul b then prf'
+      else pop_until prf' bul
+
     let put p bul =
-      if has_bullet bul p then
-	Proof.transaction p begin fun () ->
-	  while bul <> pop p do () done;
+      try
+	if not (has_bullet bul p) then
+	  (* bullet is not in use, so pushing it is always ok unless
+	     no goal under focus. *)
 	  push bul p
-	end
-      else 
-	push bul p
+	else
+	  match suggest_bullet p with
+	  | Suggest suggested_bullet when bullet_eq bul suggested_bullet
+	      -> (* suggested_bullet is mandatory and you gave the right one *)
+	    let p' = pop_until p bul in
+	    push bul p'
+	(* the bullet you gave is in use but not the right one *)
+	  | sugg -> raise (FailedBullet (bul,sugg))
+      with Proof.NoSuchGoals _ -> (* push went bad *)
+	raise (FailedBullet (bul,suggest_bullet p))
 
     let strict = {
       name = "Strict Subproofs";
-      put = put
+      put = put;
+      suggest = (fun prf -> suggest_on_solved_goal (suggest_bullet prf))
+
     }
     let _ = register_behavior strict
   end
 
   (* Current bullet behavior, controled by the option *)
   let current_behavior = ref Strict.strict
-    
+
   let _ =
     Goptions.declare_string_option {Goptions.
       optsync = true;
@@ -402,16 +579,77 @@ module Bullet = struct
 
   let put p b =
     (!current_behavior).put p b
+
+  let suggest p =
+    (!current_behavior).suggest p
 end
 
 
+let _ =
+  let hook n =
+    let prf = give_me_the_proof () in
+    (Bullet.suggest prf) in
+  Proofview.set_nosuchgoals_hook hook
+
+
+(**********************************************************)
+(*                                                        *)
+(*                     Default goal selector              *)
+(*                                                        *)
+(**********************************************************)
+
+
+(* Default goal selector: selector chosen when a tactic is applied
+   without an explicit selector. *)
+let default_goal_selector = ref (Vernacexpr.SelectNth 1)
+let get_default_goal_selector () = !default_goal_selector
+
+let print_goal_selector = function
+  | Vernacexpr.SelectAll -> "all"
+  | Vernacexpr.SelectNth i -> string_of_int i
+  | Vernacexpr.SelectId id -> Id.to_string id
+  | Vernacexpr.SelectAllParallel -> "par"
+
+let parse_goal_selector = function
+  | "all" -> Vernacexpr.SelectAll
+  | i ->
+      let err_msg = "A selector must be \"all\" or a natural number." in
+      begin try
+              let i = int_of_string i in
+              if i < 0 then Errors.error err_msg;
+              Vernacexpr.SelectNth i
+        with Failure _ -> Errors.error err_msg
+      end
+
+let _ =
+  Goptions.declare_string_option {Goptions.
+                                  optsync = true ;
+                                  optdepr = false;
+                                  optname = "default goal selector" ;
+                                  optkey = ["Default";"Goal";"Selector"] ;
+                                  optread = begin fun () -> print_goal_selector !default_goal_selector end;
+                                  optwrite = begin fun n ->
+                                    default_goal_selector := parse_goal_selector n
+                                  end
+                                 }
+
+
 module V82 = struct
   let get_current_initial_conclusions () =
-    let p = give_me_the_proof () in
-    let id = get_current_proof_name () in
-    let { strength=str ; hook=hook } = 
-      Idmap.find id !proof_info
-    in
-    (id,(Proof.V82.get_initial_conclusions p, str, hook))
+  let { pid; strength; proof } = cur_pstate () in
+  let initial = Proof.initial_goals proof in
+  let goals = List.map (fun (o, c) -> c) initial in
+    pid, (goals, strength)
 end
 
+type state = pstate list
+        
+let freeze ~marshallable =
+  match marshallable with
+  | `Yes ->
+      Errors.anomaly (Pp.str"full marshalling of proof state not supported")
+  | `Shallow -> !pstates
+  | `No -> !pstates
+let unfreeze s = pstates := s; update_proof_mode ()
+let proof_of_state = function { proof }::_ -> proof | _ -> raise NoCurrentProof
+