diff options
| -rw-r--r-- | contrib/correctness/psyntax.ml4 | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/contrib/correctness/psyntax.ml4 b/contrib/correctness/psyntax.ml4 index 33f84013d7..22c7e204a5 100644 --- a/contrib/correctness/psyntax.ml4 +++ b/contrib/correctness/psyntax.ml4 @@ -145,7 +145,7 @@ let bool_not loc a = let d = SApp ( [Variable connective_not ], [a]) in w d -let ast_zwf_zero loc = mk_appl loc loc "Zwf" [mk_ref loc "ZERO"] +let ast_zwf_zero loc = mk_appl loc loc "Zwf" [mk_ref loc "Z0"] (* program -> Coq AST *) |