diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-09-09 13:31:10 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-09-09 13:31:10 +0000 |
| commit | 2e2fe65aa3a4cc133c019c242352b2d58c624a0a (patch) | |
| tree | ed317535979bd20dfd7ed2a69ccd02335beb1ce9 /proofs | |
| parent | e46a0b49164e5e4f406a22ef66de02dd6a96c3b1 (diff) | |
Correction bug assert (introduit dans la révision 11300) qui ne
vérifiait plus si le nom de l'hyp était déjà utilisé.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11393 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/logic.ml | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/proofs/logic.ml b/proofs/logic.ml index c07b6a800..81b4a5e19 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -420,7 +420,9 @@ let prim_refiner r sigma goal = nexthyp, cl,sigma else - (push_named_context_val (id,None,t) sign),cl,sigma in + (if !check && mem_named_context id (named_context_of_val sign) then + error "New variable is already declared"; + push_named_context_val (id,None,t) sign,cl,sigma) in let sg2 = mk_goal sign cl in if b then ([sg1;sg2],sigma) else ([sg2;sg1],sigma) |