aboutsummaryrefslogtreecommitdiffstats
path: root/src/verit/veritSyntax.ml
diff options
context:
space:
mode:
Diffstat (limited to 'src/verit/veritSyntax.ml')
-rw-r--r--src/verit/veritSyntax.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/verit/veritSyntax.ml b/src/verit/veritSyntax.ml
index 21c10e8..c5db594 100644
--- a/src/verit/veritSyntax.ml
+++ b/src/verit/veritSyntax.ml
@@ -493,7 +493,7 @@ let mk_clause (id,typ,value,ids_params) =
let mk_clause cl =
try mk_clause cl
with Failure f ->
- Structures.error ("SMTCoq was not able to check the certificate \
+ CoqInterface.error ("SMTCoq was not able to check the certificate \
for the following reason.\n"^f)
let apply_dec f (decl, a) = decl, f a