|
(* This was fixed at some time, suspectingly in PR #6328 *)
Inductive foo := F (a : forall var : Type -> Type, unit -> var unit) (_ : a = a).
Goal foo.
eexists (fun var => fun u : unit => ltac:(clear u)).
shelve.
Unshelve.
all:[ > | ].
shelve.
Fail Grab Existential Variables.
Abort.
¤ Dauer der Verarbeitung: 0.15 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
