diff options
| author |  Pierre Boutillier <pierre.boutillier@ens-lyon.org> | 2014-04-10 15:59:45 +0200 |
|---|---|---|
| committer | Pierre Boutillier <pierre.boutillier@ens-lyon.org> | 2014-04-10 16:25:08 +0200 |
| commit | 29de26213adaa8b75320bee6897218d5e8d54663 (patch) | |
| tree | 85b703db6834ee0e086c81143f2463527653c354 /test-suite/bugs | |
| parent | 6e66d8c551b5edcb33a9f3fbf744b2f82d944c50 (diff) | |
By resolution of the CoqWG, instantiate must not be used now that refine works
Diffstat (limited to 'test-suite/bugs')
| -rw-r--r-- | test-suite/bugs/closed/1041.v | 13 |
1 files changed, 0 insertions, 13 deletions
diff --git a/test-suite/bugs/closed/1041.v b/test-suite/bugs/closed/1041.v deleted file mode 100644 index a5de82e0d..000000000 --- a/test-suite/bugs/closed/1041.v +++ /dev/null @@ -1,13 +0,0 @@ -Goal Prop. - -pose (P:=(fun x y :Prop => y)). -evar (Q: (forall X Y,P X Y -> Prop)) . - -instantiate (1:= fun _ => _ ) in (Value of Q). -instantiate (1:= fun _ => _ ) in (Value of Q). -instantiate (1:= fun _ => _ ) in (Value of Q). - -instantiate (1:=H) in (Value of Q). - -Admitted. - |