From 6bd490a9a3570fbb6f8a5979aaf4cd3ada3131d1 Mon Sep 17 00:00:00 2001
From: Thomas Bauereiss
Date: Fri, 16 Feb 2018 20:04:17 +0000
Subject: Avoid nested explicit type annotations

Isabelle does not like nested annotations like "((exp :: typ) :: typ)".
---
 src/rewriter.mli | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'src/rewriter.mli')

diff --git a/src/rewriter.mli b/src/rewriter.mli
index b830bdeb..08241a4b 100644
--- a/src/rewriter.mli
+++ b/src/rewriter.mli
@@ -204,6 +204,8 @@ val compute_exp_alg : 'b -> ('b -> 'b -> 'b) ->
 
 val simple_annot : Parse_ast.l -> typ -> Parse_ast.l * tannot
 
+val add_p_typ : typ -> tannot pat -> tannot pat
+
 val union_eff_exps : (tannot exp) list -> effect
 
 val fix_eff_exp : tannot exp -> tannot exp
-- 
cgit v1.2.3