diff options
| author | Pierre-Marie Pédrot | 2018-05-30 22:35:56 +0200 |
|---|---|---|
| committer | GitHub | 2018-05-30 22:35:56 +0200 |
| commit | 1103a3f909b070a54d8fe2765b274aa7d217ec91 (patch) | |
| tree | a0e15e5361f5f325fabc5b4bf2fb5dee29d925a9 /src | |
| parent | da142cf79f44c163db9c290947b34860ac902832 (diff) | |
| parent | 1cd62aa20ba3f9fb206f2926c8e47dd463dee863 (diff) | |
Merge pull request coq/ltac2#60 from ejgallego/vernac+move_parser
Adapt to coq/coq#7558.
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 |