From 01fab6cc4ec34a46b28075a82abdf740a10dea73 Mon Sep 17 00:00:00 2001
From: David Hauzar <hauzar@moloch.lri.fr>
Date: Fri, 11 Dec 2015 14:19:47 +0100
Subject: [PATCH] Add the argument of Call_provers.Unknown giving the reason of
answer Unknown.
---
src/coq-tactic/why3tac.ml4 | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/src/coq-tactic/why3tac.ml4 b/src/coq-tactic/why3tac.ml4
index c3ecb3111d..fb371d81c2 100644
--- a/src/coq-tactic/why3tac.ml4
+++ b/src/coq-tactic/why3tac.ml4
@@ -1285,7 +1285,7 @@ let why3tac ?(timelimit=timelimit) s gl =
match res.pr_answer with
| Valid -> admit_as_an_axiom gl
| Invalid -> error "Invalid"
- | Unknown s -> error ("Don't know: " ^ s)
+ | Call_provers.Unknown (s, _) -> error ("Don't know: " ^ s)
| Call_provers.Failure s -> error ("Failure: " ^ s)
| Call_provers.Timeout -> error "Timeout"
| OutOfMemory -> error "Out Of Memory"
--
GitLab