Quelle  good.mlg   Sprache: unbekannt

DECLARE PLUGIN "coq-test-suite.good"

{

let state = Summary.ref ~local:true
  ~name:"elpi-compiler-cache"
  None

}

VERNAC COMMAND EXTEND magic CLASSIFIED AS SIDEFF
| [ "magic" ] -> {
    state := Some (fun () -> ())
}
END