From b135398867bf04da57eac57df29e3136f8a0f14e Mon Sep 17 00:00:00 2001
From: herbelin
Date: Thu, 13 Jun 2002 17:57:10 +0000
Subject: Bug non vérification non redondance par Cut

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2784 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 proofs/logic.ml | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/proofs/logic.ml b/proofs/logic.ml
index 2391ece78a..5db2ec0abe 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -441,6 +441,8 @@ let prim_refiner r sigma goal =
 	       else anomaly "Intro_replacing: expects a product")
 	
     | Cut (b,id,t) ->
+    	if !check && mem_named_context id sign then
+	  error "New variable is already declared";
         if occur_meta t then error_use_instantiate();
         let sg1 = mk_goal sign (nf_betaiota t) in
         let sg2 = mk_goal (add_named_decl (id,None,t) sign) cl in
-- 
cgit v1.2.3