diff options
Diffstat (limited to 'contrib/correctness/psyntax.ml4')
| -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 72b609b24..bb9a355c3 100644 --- a/contrib/correctness/psyntax.ml4 +++ b/contrib/correctness/psyntax.ml4 @@ -787,7 +787,7 @@ END VERNAC COMMAND EXTEND Correctness [ "Correctness" preident(str) program(pgm) then_tac(tac) ] - -> [ Ptactic.correctness str pgm (option_map Tacinterp.interp tac) ] + -> [ Ptactic.correctness str pgm (Option.map Tacinterp.interp tac) ] END (* Show Programs *) |