From d99b3aa7027a6d05d238f387fa2a629b91690ea9 Mon Sep 17 00:00:00 2001
From: Chantal Keller <Chantal.Keller@lri.fr>
Date: Wed, 28 Apr 2021 20:17:16 +0200
Subject: Solve a bug when reifying under a binder

---
 src/trace/smtAtom.mli | 1 +
 1 file changed, 1 insertion(+)

(limited to 'src/trace/smtAtom.mli')

diff --git a/src/trace/smtAtom.mli b/src/trace/smtAtom.mli
index 17a0cd0..37fcd88 100644
--- a/src/trace/smtAtom.mli
+++ b/src/trace/smtAtom.mli
@@ -140,6 +140,7 @@ module Atom :
       val print_atoms : reify_tbl -> string -> unit
 
       (** Given a coq term, build the corresponding atom *)
+      exception UnknownUnderForall
       val of_coq : ?eqsym:bool -> SmtBtype.reify_tbl -> Op.reify_tbl ->
         reify_tbl -> SmtMisc.logic -> Environ.env -> Evd.evar_map -> Structures.constr -> t
 
-- 
cgit