diff options
Diffstat (limited to 'proofs/logic.ml')
| -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) |