diff options
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/derive/g_derive.mlg | 2 | ||||
| -rw-r--r-- | plugins/funind/g_indfun.mlg | 2 | ||||
| -rw-r--r-- | plugins/ltac/g_ltac.mlg | 11 | ||||
| -rw-r--r-- | plugins/ltac/g_obligations.mlg | 2 | ||||
| -rw-r--r-- | plugins/ltac/g_rewrite.mlg | 4 |
5 files changed, 7 insertions, 14 deletions
diff --git a/plugins/derive/g_derive.mlg b/plugins/derive/g_derive.mlg index df4b647642..0cdf8fb5d8 100644 --- a/plugins/derive/g_derive.mlg +++ b/plugins/derive/g_derive.mlg @@ -18,7 +18,7 @@ DECLARE PLUGIN "derive_plugin" { -let classify_derive_command _ = Vernacextend.(VtStartProof ("Classic",Doesn'tGuaranteeOpacity,[]),VtLater) +let classify_derive_command _ = Vernacextend.(VtStartProof (Doesn'tGuaranteeOpacity,[]),VtLater) } diff --git a/plugins/funind/g_indfun.mlg b/plugins/funind/g_indfun.mlg index 8f0440a2a4..c4f8843e51 100644 --- a/plugins/funind/g_indfun.mlg +++ b/plugins/funind/g_indfun.mlg @@ -186,7 +186,7 @@ VERNAC COMMAND EXTEND Function (Vernacexpr.(VernacExpr([], VernacFixpoint(Decl_kinds.NoDischarge, List.map snd recsl)))) with | Vernacextend.VtSideff ids, _ when hard -> - Vernacextend.(VtStartProof ("Classic", GuaranteesOpacity, ids), VtLater) + Vernacextend.(VtStartProof (GuaranteesOpacity, ids), VtLater) | x -> x } -> { do_generate_principle false (List.map snd recsl) } END diff --git a/plugins/ltac/g_ltac.mlg b/plugins/ltac/g_ltac.mlg index d9b19c1ae6..4c24f51b1e 100644 --- a/plugins/ltac/g_ltac.mlg +++ b/plugins/ltac/g_ltac.mlg @@ -58,15 +58,8 @@ let new_entry name = let toplevel_selector = new_entry "vernac:toplevel_selector" let tacdef_body = new_entry "tactic:tacdef_body" -(* Registers the Classic Proof Mode (which uses [tactic_mode] as a parser for - proof editing and changes nothing else). Then sets it as the default proof mode. *) -let _ = - let mode = { - Proof_global.name = "Classic"; - set = (fun () -> Pvernac.set_command_entry tactic_mode); - reset = (fun () -> Pvernac.(set_command_entry noedit_mode)); - } in - Proof_global.register_proof_mode mode +(* Registers [tactic_mode] as a parser for proof editing *) +let classic_proof_mode = Pvernac.register_proof_mode "Classic" tactic_mode (* Hack to parse "[ id" without dropping [ *) let test_bracket_ident = diff --git a/plugins/ltac/g_obligations.mlg b/plugins/ltac/g_obligations.mlg index 1ea6ff84d4..cdee012a82 100644 --- a/plugins/ltac/g_obligations.mlg +++ b/plugins/ltac/g_obligations.mlg @@ -83,7 +83,7 @@ open Obligations let obligation obl tac = with_tac (fun t -> Obligations.obligation obl t) tac let next_obligation obl tac = with_tac (fun t -> Obligations.next_obligation obl t) tac -let classify_obbl _ = Vernacextend.(VtStartProof ("Classic",Doesn'tGuaranteeOpacity,[]), VtLater) +let classify_obbl _ = Vernacextend.(VtStartProof (Doesn'tGuaranteeOpacity,[]), VtLater) } diff --git a/plugins/ltac/g_rewrite.mlg b/plugins/ltac/g_rewrite.mlg index 31fb1c9abf..db8d1b20d8 100644 --- a/plugins/ltac/g_rewrite.mlg +++ b/plugins/ltac/g_rewrite.mlg @@ -285,13 +285,13 @@ VERNAC COMMAND EXTEND AddSetoid1 CLASSIFIED AS SIDEFF add_morphism_infer atts m n; } | #[ atts = rewrite_attributes; ] [ "Add" "Morphism" constr(m) "with" "signature" lconstr(s) "as" ident(n) ] - => { VtStartProof("Classic",GuaranteesOpacity,[n]), VtLater } + => { VtStartProof(GuaranteesOpacity,[n]), VtLater } -> { add_morphism atts [] m s n; } | #[ atts = rewrite_attributes; ] [ "Add" "Parametric" "Morphism" binders(binders) ":" constr(m) "with" "signature" lconstr(s) "as" ident(n) ] - => { VtStartProof("Classic",GuaranteesOpacity,[n]), VtLater } + => { VtStartProof(GuaranteesOpacity,[n]), VtLater } -> { add_morphism atts binders m s n; } |