From 3328d1f56c12f4f4618f2d2668092c1a44160f0d Mon Sep 17 00:00:00 2001
From: aspiwack
Date: Fri, 6 Jan 2012 13:24:00 +0000
Subject: 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
---
 proofs/proof_global.ml | 11 ++++++++++-
 1 file changed, 10 insertions(+), 1 deletion(-)

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 ; 
-- 
cgit v1.2.3