Library CFML.CFHeader

Set Implicit Arguments.
Require Import LibTactics.
Require CFPrint.



Notation "'RegisterCF' T" := (ltac_database (boxer CFPrint.database_cf) (boxer T) _)
  (at level 69, T at level 0) : cfheader_scope.

Ltac CFHeader_Provide T := Provide T.