From 0a84134bdd686e3dc0846df6b33d0610cf75c149 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 9 Jun 2010 10:09:05 +0000
Subject: Automatic introduction of names given before ":" in Lemma's and
 Definition's is not so painless. It seems to however generally provide
 "nicer" scripts so let us keep it and update the contribs and test-suite
 accordingly. Also enforced that the actual introduced names to be exactly as
 given in the statements.

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

(limited to 'proofs')

diff --git a/proofs/logic.ml b/proofs/logic.ml
index 840c71ec6f..db60c6afc0 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -481,7 +481,7 @@ let prim_refiner r sigma goal =
     (* Logical rules *)
     | Intro id ->
     	if !check && mem_named_context id (named_context_of_val sign) then
-	  error "New variable is already declared";
+	  error ("Variable " ^ string_of_id id ^ " is already declared.");
         (match kind_of_term (strip_outer_cast cl) with
 	   | Prod (_,c1,b) ->
 	       let (sg,ev,sigma) = mk_goal (push_named_context_val (id,None,c1) sign)
@@ -510,7 +510,7 @@ let prim_refiner r sigma goal =
 	      cl,sigma
 	  else
             (if !check && mem_named_context id (named_context_of_val sign) then
-                error "New variable is already declared";
+	      error ("Variable " ^ string_of_id id ^ " is already declared.");
 	     push_named_context_val (id,None,t) sign,cl,sigma) in
         let (sg2,ev2,sigma) = 
 	  Goal.V82.mk_goal sigma sign cl (Goal.V82.extra sigma goal) in
-- 
cgit v1.2.3