Opened 14 years ago
Closed 14 years ago
#368 closed defect (needmoreinfo)
coq, already defined values
| Reported by: | Damien Pous | Owned by: | David Aspinall |
|---|---|---|---|
| Priority: | major | Milestone: | PG-Emacs-4.0 |
| Component: | 7:prover-coq | Keywords: | already defined |
| Cc: |
Description
Hi,
The following code is rejected by Coq, since [x] is already defined in the second line, but proofgeneral "validates" it (it goes through, so that one has to be really careful to notice the warning in the "coq output" buffer - this can be quite errorprone since Coq keeps the old definition).
<< Definition x := 3. Definition x := 5.
Damien
Change History (1)
comment:1 Changed 14 years ago by
| Resolution: | → needmoreinfo |
|---|---|
| Status: | new → closed |
Note: See
TracTickets for help on using
tickets.
Thanks for the report. Unfortunately I can't reproduce this, using Ubuntu with standard packages for Emacs and Coq and PG CVS. Can you tell me your version numbers?