From d99b3aa7027a6d05d238f387fa2a629b91690ea9 Mon Sep 17 00:00:00 2001 From: Chantal Keller Date: Wed, 28 Apr 2021 20:17:16 +0200 Subject: Solve a bug when reifying under a binder --- src/trace/smtAtom.ml | 13 +++++++++++-- 1 file changed, 11 insertions(+), 2 deletions(-) (limited to 'src/trace/smtAtom.ml') diff --git a/src/trace/smtAtom.ml b/src/trace/smtAtom.ml index 62cbe99..ff6db6a 100644 --- a/src/trace/smtAtom.ml +++ b/src/trace/smtAtom.ml @@ -1096,6 +1096,8 @@ module Atom = Hashtbl.find op_coq_terms + exception UnknownUnderForall + let of_coq ?eqsym:(eqsym=false) rt ro reify known_logic env sigma c = let op_tbl = Lazy.force op_tbl in let get_cst c = @@ -1361,10 +1363,17 @@ module Atom = let i = Structures.destRel c in let n, _ = Structures.destruct_rel_decl (Environ.lookup_rel i env) in Some (Structures.string_of_name n) - else + else if Vars.closed0 c then None + else + (* Uninterpreted expression depending on a quantified variable. + We do not handle it for the moment. + We leave for future work to have "dependent" constants. + *) + raise UnknownUnderForall in - Op.declare ro c targs tres os in + Op.declare ro c targs tres os + in (try let (i, _) = destruct "" op in Hashtbl.add op_coq_terms i c (* Chantal: I think we should move it to "Not_found" (otherwise it is already in the table) *) -- cgit