Proofrecording/tools/init.ml

   1 (* ------------------------------------------------------------------------- *)
   2 (* Set up a quotation expander for my `...` quotes.                          *)
   3 (* ------------------------------------------------------------------------- *)
   4
   5 let quotexpander s =
   6   if String.sub s 0 1 = ":" then
   7     "parse_type \""^
   8     (String.escaped (String.sub s 1 (String.length s - 1)))^"\""
   9   else "parse_term \""^(String.escaped s)^"\"";;
  10
  11 Quotation.add "tot" (Quotation.ExStr (fun x -> quotexpander));;