summaryrefslogtreecommitdiff
path: root/src/pretty_print_lem.ml
diff options
context:
space:
mode:
authorAlasdair Armstrong2017-09-21 18:31:49 +0100
committerAlasdair Armstrong2017-09-21 18:31:49 +0100
commit669bfc2cd34bda80e69ba6c75edbd3e4d57114cd (patch)
tree8638cbd82f46433b8ae574cb04a924735005b90c /src/pretty_print_lem.ml
parentb097466ab11fd035dbfd5c7c51ea0644c62b92da (diff)
Refactored AST valspecs into single constructor
Diffstat (limited to 'src/pretty_print_lem.ml')
-rw-r--r--src/pretty_print_lem.ml8
1 files changed, 1 insertions, 7 deletions
diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml
index 7f04c495..d40381b9 100644
--- a/src/pretty_print_lem.ml
+++ b/src/pretty_print_lem.ml
@@ -1429,13 +1429,7 @@ let doc_dec_lem sequential (DEC_aux (reg, ((l, _) as annot))) =
| DEC_alias(id,alspec) -> empty
| DEC_typ_alias(typ,id,alspec) -> empty
-let doc_spec_lem mwords (VS_aux (valspec,annot)) =
- match valspec with
- | VS_extern_no_rename _
- | VS_extern_spec _ -> empty (* ignore these at the moment *)
- | VS_val_spec (typschm,id) | VS_cast_spec (typschm,id) -> empty
-(* separate space [string "val"; doc_id_lem id; string ":";doc_typschm_lem mwords typschm] ^/^ hardline *)
-
+let doc_spec_lem mwords (VS_aux (valspec,annot)) = empty
let rec doc_def_lem sequential mwords def = match def with
| DEF_spec v_spec -> (doc_spec_lem mwords v_spec,empty)