Permalink
Browse files

Add comment for using astPP in simple_bstProg

  • Loading branch information...
xrchz committed Sep 2, 2017
1 parent b78ffcf commit 894041e6942fd6c0e60c1044c5c7b50272147ff4
Showing with 8 additions and 2 deletions.
  1. +1 −1 tutorial/Holmakefile
  2. +7 −1 tutorial/simple_bstProgScript.sml
@@ -1,3 +1,3 @@
INCLUDES = $(HOLDIR)/examples/balanced_bst ../misc ../translator ../basis/pure ../basis ../characteristic ../compiler\
../semantics/proofs ../compiler/backend/proofs ../compiler/backend/x64/proofs
../semantics ../semantics/proofs ../compiler/backend/proofs ../compiler/backend/x64/proofs
CLINE_OPTIONS = --qof
@@ -50,7 +50,13 @@ in current_prog end
(*
get_current_prog()
*)
(* TODO: it would be nice to be able to print this in concrete syntax *)

(*
To print in concrete syntax:
astPP.enable_astPP();
To remove this pretty-printing:
astPP.disable_astPP();
*)

val res = translate insert_def;

0 comments on commit 894041e

Please sign in to comment.