From 7d399ba201a023f2f148f6151d83b1569b93262f Mon Sep 17 00:00:00 2001
From: Simon Cruanes <simon.cruanes.2007@m4x.org>
Date: Tue, 18 Aug 2020 10:01:36 -0400
Subject: [PATCH] handle `:named` attribute in smtlib

---
 src/smtlib/Typecheck.ml | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/smtlib/Typecheck.ml b/src/smtlib/Typecheck.ml
index 4bc8b228..e2192a80 100644
--- a/src/smtlib/Typecheck.ml
+++ b/src/smtlib/Typecheck.ml
@@ -287,6 +287,7 @@ let rec conv_term (ctx:Ctx.t) (t:PA.term) : T.t =
       ill_typed ctx "term `%a`@ should have type `%a`" T.pp t Ty.pp ty_expect
     );
     t
+  | PA.Attr (t, [":named",_]) -> conv_term ctx t
   | _ ->
     errorf_ctx ctx "unsupported term %a" PA.pp_term t