summaryrefslogtreecommitdiff
path: root/src/rewrites.mli
diff options
context:
space:
mode:
authorAlasdair Armstrong2018-01-05 17:40:19 +0000
committerAlasdair Armstrong2018-01-05 17:40:19 +0000
commitcb796f509c412c4f354e045f7b83f233d8863181 (patch)
treee7457e59f9151710f6a5209548f7023bf2b9371e /src/rewrites.mli
parentb52a739d24e138974fada0453f3a6d514a36994c (diff)
Fix duplicate definitions created by merge
Diffstat (limited to 'src/rewrites.mli')
-rw-r--r--src/rewrites.mli3
1 files changed, 0 insertions, 3 deletions
diff --git a/src/rewrites.mli b/src/rewrites.mli
index 743774d9..8fceadff 100644
--- a/src/rewrites.mli
+++ b/src/rewrites.mli
@@ -64,9 +64,6 @@ val rewrite_defs_interpreter : (string * (tannot defs -> tannot defs)) list
val rewrite_defs_lem : (string * (tannot defs -> tannot defs)) list
(* Perform rewrites to sail intermediate language *)
-val rewrite_defs_interpreter : (string * (tannot defs -> tannot defs)) list
-
-(* Perform rewrites to sail intermediate language *)
val rewrite_defs_sil : (string * (tannot defs -> tannot defs)) list
(* This is a special rewriter pass that checks AST invariants without