diff options
| author | herbelin | 2010-06-09 10:09:05 +0000 |
|---|---|---|
| committer | herbelin | 2010-06-09 10:09:05 +0000 |
| commit | 0a84134bdd686e3dc0846df6b33d0610cf75c149 (patch) | |
| tree | f18c5b29b5361aaf250895bc3d7a3ea636494a0e /proofs | |
| parent | cb586ea65a1ad38626b7481ff8b30007f488705d (diff) | |
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
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/logic.ml | 4 |
1 files changed, 2 insertions, 2 deletions
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 |