diff options
| author | Alasdair Armstrong | 2017-09-21 16:12:12 +0100 |
|---|---|---|
| committer | Alasdair Armstrong | 2017-09-21 16:12:12 +0100 |
| commit | 3d853e394b5bb5aa0862b56cfbb068aef8d2458a (patch) | |
| tree | 7ff0629773b5e6aa4119036860d40013678484b3 /src/pretty_print_lem_ast.ml | |
| parent | f726c992ab2506ae3fb8a52993b2c46a1ae0a3b1 (diff) | |
Simplify AST by removing LB_val_explicit and replace LB_val_implicit with just LB_val in AST
also rename functions in rewriter.ml appropriately.
Diffstat (limited to 'src/pretty_print_lem_ast.ml')
| -rw-r--r-- | src/pretty_print_lem_ast.ml | 6 |
1 files changed, 2 insertions, 4 deletions
diff --git a/src/pretty_print_lem_ast.ml b/src/pretty_print_lem_ast.ml index 48ec37b8..f0f25795 100644 --- a/src/pretty_print_lem_ast.ml +++ b/src/pretty_print_lem_ast.ml @@ -349,10 +349,8 @@ let pp_lem_pat ppf p = base ppf (pp_format_pat_lem p) let rec pp_lem_let ppf (LB_aux(lb,(l,annot))) = let print_lb ppf lb = match lb with - | LB_val_explicit(ts,pat,exp) -> - fprintf ppf "@[<0>(%a %a %a %a)@]" kwd "LB_val_explicit" pp_lem_typscm ts pp_lem_pat pat pp_lem_exp exp - | LB_val_implicit(pat,exp) -> - fprintf ppf "@[<0>(%a %a %a)@]" kwd "LB_val_implicit" pp_lem_pat pat pp_lem_exp exp in + | LB_val(pat,exp) -> + fprintf ppf "@[<0>(%a %a %a)@]" kwd "LB_val" pp_lem_pat pat pp_lem_exp exp in fprintf ppf "@[<0>(LB_aux %a (%a, %a))@]" print_lb lb pp_lem_l l pp_annot annot and pp_lem_exp ppf (E_aux(e,(l,annot))) = |