Forbids (as it has always been the behaviour) to have two different open

proofs with the same name.

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

1 files changed, 10 insertions, 1 deletions

diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 2745270a65..9d5ba230e5 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -239,6 +239,11 @@ let set_proof_mode mn =
   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
@@ -248,7 +253,11 @@ let set_proof_mode mn =
     It raises exception [ProofInProgress] if there is a proof being
     currently edited. *)
 let start_proof  id str goals ?(compute_guard=[]) hook =
-  (* arnaud: ajouter une vérification pour la présence de id dans le proof_global *)
+  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 ;