Ltac2 get_opt o := match o with None => Control.throw Not_found | Some x => x end.
Goal True. Proof. (* Fails at runtime because not fully applied *)
Fail ltac1:(ltac2:(x |- ())). (* Type mismatch: Ltac1.t vs. constr *)
Fail ltac1:(ltac2:(x |- pose $x)). (* Check that runtime cast is OK *)
ltac1:(let t := ltac2:(x |- let c := (get_opt (Ltac1.to_constr x)) in pose $c) in t nat). (* Type mismatch *)
Fail ltac1:(let t := ltac2:(x |- let c := (get_opt (Ltac1.to_constr x)) in pose $c) in t ident:(foo)). Abort.
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.
