Changes between Initial Version and Version 2 of Ticket #141


Ignore:
Timestamp:
Sep 17, 2007, 1:28:27 PM (17 years ago)
Author:
David Aspinall
Comment:

Legend:

Unmodified
Added
Removed
Modified

  • Ticket #141

    • Property Status changed from new to closed
    • Property Resolution changed from to worksforme
    • Property Summary changed from Warnings in proof mode in Coq to Warnings missing in proof mode in Coq

  • Ticket #141 – Description

    initial v2  
    55For example:
    66
     7{{{
    78Goal True /\ True -> True.
    89intro H.
    910destruct H as [H1 H2 H3].
     11}}}
    1012
    1113After the last command, the minibuffer contains "[Coq] Warning: Unused introduction pattern : H3", but the *response* buffer is empty. The same happens if I process
    1214
     15{{{
    1316Require Import Setoid.
    1417Goal False.
    1518setoid_replace False with True.
     19}}}
    1620
    1721The minibuffer contains a truncated warning "[Coq] Warning: There are several relations of the carrier 'Prop'. The relation (P", but the response buffer is again empty.