Bug 2074 - reflexivity tactic ignores opacity specification for definition
: reflexivity tactic ignores opacity specification for definition
Status: RESOLVED DUPLICATE of bug 3389
Product: Coq
Classification: Unclassified
Component: Tactics
: 8.2
: All Linux
: P3 normal
: ---
Assigned To: Matthieu Sozeau
Depends on:
  Show dependency treegraph
Reported: 2009-03-09 16:29 CET by Eelis van der Weegen
Modified: 2014-08-14 15:49 CEST (History)
3 users (show)

See Also:


Note You need to log in before you can comment on or make changes to this bug.
Description Eelis van der Weegen 2009-03-09 16:29:21 CET

  Definition w: nat := 0.
  Opaque w.
  Goal w = 0. reflexivity. Qed.
It appears w's opacity is somehow ignored by reflexivity.
Comment 1 Eelis van der Weegen 2010-04-17 20:33:49 CEST
No reaction? Not even a confirmation? :(

Doesn't the testcase succinctly reveal a gaping hole in an important area of Coq functionality?..
Comment 2 Matthieu Sozeau 2010-07-28 19:41:04 CEST
Indeed, this is pretty clearly a leak.
Comment 3 Thomas Braibant 2010-09-13 13:40:31 CEST
In this piece of code, we can see that reflexivity is not the ultimate 'culprit' : apply does the same kind of things. (In 8.3-rc1 though)

Section T.
  Variable A : Type.
  Definition f (y : A) := y.
  Variable P : A -> Prop.
  Variable a : A.
  Hypothesis H : P a.
  Opaque f.
  Goal P (f a).
    simple apply H.
End T.
Comment 4 Stephane Glondu 2010-09-13 14:06:58 CEST
vm_compute seems to ignore Opaque directives as well (whereas compute does not)...
Comment 5 Matthieu Sozeau 2014-08-14 15:49:13 CEST
The Opaque directive does not make things "really" opaque, only expanded last by the conversion/unification unfolding oracle. Making definitions really ununfoldable after their definition would be very dangerous as retyping terms containing them could fail. A better way to handle this has to be found, as suggested in bug # 3389 for example.

*** This bug has been marked as a duplicate of bug 3389 ***