6 files changed, 2 insertions, 49 deletions
diff --git a/proofs/logic.ml b/proofs/logic.ml
index 1116410dc..f283d0f33 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -57,7 +57,7 @@ let is_unification_error = function
 | UnsolvableImplicit _| AbstractionOverMeta _ -> true
 | _ -> false
 
-let rec catchable_exception = function
+let catchable_exception = function
   | Errors.UserError _ | TypeError _
   | RefinerError _ | Indrec.RecursionSchemeError _
   | Nametab.GlobalizationError _
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index ca760c456..68c2ed328 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -25,9 +25,6 @@ let delete_proof = Proof_global.discard
 let delete_current_proof = Proof_global.discard_current
 let delete_all_proofs = Proof_global.discard_all
 
-let set_undo _ = ()
-let get_undo _ = None
-
 let start_proof (id : Id.t) str hyps c ?init_tac terminator =
   let goals = [ (Global.env_of_context hyps , c) ] in
   Proof_global.start_proof id str goals terminator;
@@ -132,11 +129,6 @@ let build_constant_by_tactic id sign ?(goal_kind = Global,Proof Theorem) typ tac
     delete_current_proof ();
     raise reraise
 
-let constr_of_def = function
-  | Declarations.Undef _ -> assert false
-  | Declarations.Def cs -> Mod_subst.force_constr cs
-  | Declarations.OpaqueDef lc -> Opaqueproof.force_proof lc
-
 let build_by_tactic env typ tac =
   let id = Id.of_string ("temporary_proof"^string_of_int (next())) in
   let sign = val_of_named_context (named_context env) in
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index f5431daaa..3cdecb633 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -115,32 +115,12 @@ let _ = Errors.register_handler begin function
   | NoSuchProof -> Errors.error "No such proof."
   | _ -> raise Errors.Unhandled
 end
-let extract id l =
-  let rec aux = function
-    | ({pid = id' } as np)::l when Id.equal id id' -> (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 -> 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
-
-(* combinators for the proof_info map *)
-let add id info m =
-  m := Id.Map.add id info !m
-let remove id m =
-  m := Id.Map.remove id !m
 
 (*** Proof Global manipulation ***)
 
@@ -233,12 +213,6 @@ let activate_proof_mode mode =
 let disactivate_proof_mode mode =
   Ephemeron.iter_opt (find_proof_mode mode) (fun x -> x.reset ())
 
-exception AlreadyExists
-let _ = Errors.register_handler begin function
-  | AlreadyExists -> Errors.error "Already editing something of that name."
-  | _ -> raise Errors.Unhandled
-end
-
 (** [start_proof 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
diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli
index 0635f03d0..47d63e2eb 100644
--- a/proofs/proof_global.mli
+++ b/proofs/proof_global.mli
@@ -121,10 +121,6 @@ val set_interp_tac :
 val set_used_variables : Names.Id.t list -> unit
 val get_used_variables : unit -> Context.section_context option
 
-val discard : Names.identifier Loc.located -> unit
-val discard_current : unit -> unit
-val discard_all : unit -> unit
-
 (**********************************************************)
 (*                                                        *)
 (*                            Proof modes                 *)
diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index 76af0c1e0..1365fe86e 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -223,7 +223,7 @@ let apply env t sp =
 (*** tacticals ***)
 
 
-let rec catchable_exception = function
+let catchable_exception = function
   | Proof_errors.Exception _ -> false
   | e -> Errors.noncritical e
 
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index 3c3bb3970..609428792 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -98,10 +98,6 @@ let thensi_tac tac (sigr,gs) =
 
 let then_tac tac = thensf_tac [||] tac
 
-let non_existent_goal n =
-  errorlabstrm ("No such goal: "^(string_of_int n))
-    (str"Trying to apply a tactic to a non existent goal")
-
 (* [tclTHENS3PARTS tac1 [|t1 ; ... ; tn|] tac2 [|t'1 ; ... ; t'm|] gls]
    applies the tactic [tac1] to [gls] then, applies [t1], ..., [tn] to
    the first [n] resulting subgoals, [t'1], ..., [t'm] to the last [m]
@@ -370,11 +366,6 @@ let tactic_list_tactic tac gls =
 (* Change evars *)
 let tclEVARS sigma gls = tclIDTAC {gls with sigma=sigma}
 
-(* Pretty-printers. *)
-
-let pp_info = ref (fun _ _ _ -> assert false)
-let set_info_printer f = pp_info := f
-
 (* Check that holes in arguments have been resolved *)
 
 let check_evars env sigma extsigma origsigma =