diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-03-10 15:20:47 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-03-19 01:36:22 +0100 |
| commit | d94a8b2024497e11ff9392a7fa4401ffcc131cc0 (patch) | |
| tree | 16bc882982b19a6188ddd0b25c6a76820ea02cf8 /parsing/g_vernac.ml4 | |
| parent | a11dd2209f47b6b79ace3d32071d29bd5652e07a (diff) | |
Moving the proof mode parsing management to Pcoq.
Diffstat (limited to 'parsing/g_vernac.ml4')
| -rw-r--r-- | parsing/g_vernac.ml4 | 12 |
1 files changed, 1 insertions, 11 deletions
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 49baeb556..2eb590132 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -35,7 +35,6 @@ let _ = List.iter Lexer.add_keyword vernac_kw let query_command = Gram.entry_create "vernac:query_command" let tactic_mode = Gram.entry_create "vernac:tactic_command" -let noedit_mode = Gram.entry_create "vernac:noedit_command" let subprf = Gram.entry_create "vernac:subprf" let class_rawexpr = Gram.entry_create "vernac:class_rawexpr" @@ -48,11 +47,6 @@ let subgoal_command = Gram.entry_create "proof_mode:subgoal_command" let instance_name = Gram.entry_create "vernac:instance_name" let section_subset_expr = Gram.entry_create "vernac:section_subset_expr" -let command_entry = ref noedit_mode -let set_command_entry e = command_entry := e -let get_command_entry () = !command_entry - - (* 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 set_tactic_mode () = set_command_entry tactic_mode @@ -82,10 +76,6 @@ let test_bracket_ident = | _ -> raise Stream.Failure) | _ -> raise Stream.Failure) -let default_command_entry = - Gram.Entry.of_parser "command_entry" - (fun strm -> Gram.parse_tokens_after_filter (get_command_entry ()) strm) - GEXTEND Gram GLOBAL: vernac gallina_ext tactic_mode noedit_mode subprf subgoal_command; vernac: FIRST @@ -129,7 +119,7 @@ GEXTEND Gram ] ] ; vernac_aux: LAST - [ [ prfcom = default_command_entry -> prfcom ] ] + [ [ prfcom = command_entry -> prfcom ] ] ; noedit_mode: [ [ c = subgoal_command -> c None] ] |