~~~coq Require Import Ltac2.Ltac2. Module M. Local Ltac2 Type exn ::= [ E ]. Ltac2 e := E. End M. Ltac2 Eval M.e. (* anomaly uncaught not_found *) ~~~