File: open_constr.v

package info (click to toggle)
coq 8.9.0-1
  • links: PTS, VCS
  • area: main
  • in suites: buster
  • size: 30,604 kB
  • sloc: ml: 192,230; sh: 2,585; python: 2,206; ansic: 1,878; makefile: 818; lisp: 202; xml: 24; sed: 2
file content (12 lines) | stat: -rw-r--r-- 293 bytes parent folder | download | duplicates (3)
1
2
3
4
5
6
7
8
9
10
11
12
Tactic Notation "opose" open_constr(foo) := pose foo.
Class Foo := Build_Foo : Set.
Axiom f : forall `{Foo}, Set.
Set Printing Implicit.
Goal forall `{Foo}, True.
Proof.
  intro H.
  pose f.
  opose f.
  Fail let x := (eval hnf in P) in has_evar x.
  let x := (eval hnf in P0) in has_evar x.