diff options
| author | herbelin | 2002-06-13 17:57:10 +0000 |
|---|---|---|
| committer | herbelin | 2002-06-13 17:57:10 +0000 |
| commit | b135398867bf04da57eac57df29e3136f8a0f14e (patch) | |
| tree | 84f7d13ee79e9d592e80d6917e077d5b9d925e0f | |
| parent | 48410baeddcb756ec0fd2dec1cd41e3f35e58dfa (diff) | |
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
| -rw-r--r-- | proofs/logic.ml | 2 |
1 files changed, 2 insertions, 0 deletions
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 |