blob: 743e62932d34d7b598d1a9e13abec0a21aab3143 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
|
Require Import Ltac2.Ltac2.
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.
|
