diff options
| author | Chantal Keller <Chantal.Keller@lri.fr> | 2021-04-28 20:17:16 +0200 |
|---|---|---|
| committer | Chantal Keller <Chantal.Keller@lri.fr> | 2021-04-28 20:17:16 +0200 |
| commit | d99b3aa7027a6d05d238f387fa2a629b91690ea9 (patch) | |
| tree | 2892ff5be52b7e0d6fe3e079bf5fcb302090edaf /src/trace/smtAtom.ml | |
| parent | 34f32c6ac00a9c385baf65861d367e0e1006c1ab (diff) | |
| download | smtcoq-d99b3aa7027a6d05d238f387fa2a629b91690ea9.tar.gz smtcoq-d99b3aa7027a6d05d238f387fa2a629b91690ea9.zip | |
Solve a bug when reifying under a binder
Diffstat (limited to 'src/trace/smtAtom.ml')
| -rw-r--r-- | src/trace/smtAtom.ml | 13 |
1 files changed, 11 insertions, 2 deletions
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) *) |