summaryrefslogtreecommitdiff
path: root/src/pretty_print_lem.ml
diff options
context:
space:
mode:
authorThomas Bauereiss2017-12-06 17:18:36 +0000
committerThomas Bauereiss2017-12-06 17:18:36 +0000
commit2bc281428a3a1d608d56f69e71b50056a25e3da0 (patch)
treedfd8e8a13702696fd9daef64315952b9652f95e8 /src/pretty_print_lem.ml
parentc3c3c40a1d4f81448d8356317e88be2b04363df7 (diff)
parent44e9396fa90ab68ee4c8d9674c6bbad6fc851c6d (diff)
Merge remote branch 'experiments' into experiments
Diffstat (limited to 'src/pretty_print_lem.ml')
-rw-r--r--src/pretty_print_lem.ml8
1 files changed, 7 insertions, 1 deletions
diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml
index f5f58d14..7ced47ee 100644
--- a/src/pretty_print_lem.ml
+++ b/src/pretty_print_lem.ml
@@ -9,7 +9,14 @@
(* Robert Norton-Wright *)
(* Christopher Pulte *)
(* Peter Sewell *)
+(* Alasdair Armstrong *)
+(* Brian Campbell *)
(* Thomas Bauereiss *)
+(* Anthony Fox *)
+(* Jon French *)
+(* Dominic Mulligan *)
+(* Stephen Kell *)
+(* Mark Wassell *)
(* *)
(* All rights reserved. *)
(* *)
@@ -1192,7 +1199,6 @@ let doc_typdef_lem sequential mwords (TD_aux(td, (l, annot))) = match td with
break 0 ^^ brackets (align doc_rids)]))
| _ -> raise (Reporting_basic.err_unreachable l "register with non-constant indices")
-
let doc_rec_lem (Rec_aux(r,_)) = match r with
| Rec_nonrec -> space
| Rec_rec -> space ^^ string "rec" ^^ space