diff options
| author | Emilio Jesus Gallego Arias | 2018-05-20 21:15:44 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-05-27 17:13:32 +0200 |
| commit | 1cd62aa20ba3f9fb206f2926c8e47dd463dee863 (patch) | |
| tree | 5bd59b5a707a0e1aec7a34aa66ecda1136dc0607 /src | |
| parent | e15c228709351f5001f6a10765a816cebcf900cc (diff) | |
Adapt to coq/coq#7558.
Trivial renaming of the vernacular parsing entry point.
Diffstat (limited to 'src')
| -rw-r--r-- | src/g_ltac2.ml4 | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/g_ltac2.ml4 b/src/g_ltac2.ml4 index 6189bb18cc..ac65495fe5 100644 --- a/src/g_ltac2.ml4 +++ b/src/g_ltac2.ml4 @@ -841,8 +841,8 @@ END let _ = let mode = { Proof_global.name = "Ltac2"; - set = (fun () -> set_command_entry tac2mode); - reset = (fun () -> set_command_entry Pcoq.Vernac_.noedit_mode); + set = (fun () -> Pvernac.set_command_entry tac2mode); + reset = (fun () -> Pvernac.(set_command_entry Vernac_.noedit_mode)); } in Proof_global.register_proof_mode mode |