File: ltac2env.v

package info (click to toggle)
coq 8.20.1%2Bdfsg-1
  • links: PTS, VCS
  • area: main
  • in suites: sid, trixie
  • size: 44,116 kB
  • sloc: ml: 234,160; sh: 4,301; python: 3,270; ansic: 2,644; makefile: 882; lisp: 172; javascript: 63; xml: 24; sed: 2
file content (15 lines) | stat: -rw-r--r-- 541 bytes parent folder | download | duplicates (5) 
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.