diff options
| author | Pierre-Marie Pédrot | 2014-02-16 04:17:30 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2014-02-16 14:36:15 +0100 |
| commit | abd83cffe1afe6745775c67b8c827038e295a1d2 (patch) | |
| tree | 047668419f552be8e803cd6e558bae917c5d49e6 /plugins/decl_mode | |
| parent | f4d6b4bce315639008b52727f741de82e2687d7e (diff) | |
Removing non-marshallable data from the Agram constructor. Instead of
containing opaque grammar objects, it now contains a string representing
the entry. In order to recover the entry from the string, the former must
have been created with [Pcoq.create_generic_entry] or similar. This is
guaranteed for entries generated by ARGUMENT EXTEND, and must be done by
hand otherwise.
Some plugins were fixed accordingly.
Diffstat (limited to 'plugins/decl_mode')
| -rw-r--r-- | plugins/decl_mode/g_decl_mode.ml4 | 16 |
1 files changed, 8 insertions, 8 deletions
diff --git a/plugins/decl_mode/g_decl_mode.ml4 b/plugins/decl_mode/g_decl_mode.ml4 index 216d88e66d..fe75d17f6a 100644 --- a/plugins/decl_mode/g_decl_mode.ml4 +++ b/plugins/decl_mode/g_decl_mode.ml4 @@ -83,14 +83,6 @@ let vernac_proof_instr instr = Vernacentries.print_subgoals () end -(* We create a new parser entry [proof_mode]. The Declarative proof mode - will replace the normal parser entry for tactics with this one. *) -let proof_mode : vernac_expr Gram.entry = - Gram.entry_create "vernac:proof_command" -(* Auxiliary grammar entry. *) -let proof_instr : raw_proof_instr Gram.entry = - Gram.entry_create "proofmode:instr" - (* Before we can write an new toplevel command (see below) which takes a [proof_instr] as argument, we need to declare how to parse it, print it, globalise it and interprete it. @@ -103,6 +95,14 @@ let proof_instr : raw_proof_instr Gram.entry = let wit_proof_instr : (raw_proof_instr, Empty.t, Empty.t) Genarg.genarg_type = Genarg.make0 None "proof_instr" +(* We create a new parser entry [proof_mode]. The Declarative proof mode + will replace the normal parser entry for tactics with this one. *) +let proof_mode : vernac_expr Gram.entry = + Gram.entry_create "vernac:proof_command" +(* Auxiliary grammar entry. *) +let proof_instr : raw_proof_instr Gram.entry = + Pcoq.create_generic_entry "proof_instr" (Genarg.rawwit wit_proof_instr) + let _ = Pptactic.declare_extra_genarg_pprule wit_proof_instr pr_raw_proof_instr pr_glob_proof_instr pr_proof_instr |