diff options
Diffstat (limited to 'plugins/decl_mode')
| -rw-r--r-- | plugins/decl_mode/g_decl_mode.ml4 | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/decl_mode/g_decl_mode.ml4 b/plugins/decl_mode/g_decl_mode.ml4 index 88e62e46df..b5a2ac82eb 100644 --- a/plugins/decl_mode/g_decl_mode.ml4 +++ b/plugins/decl_mode/g_decl_mode.ml4 @@ -103,7 +103,7 @@ let proof_instr = Gram.entry_create "proofmode:instr" (* [Genarg.create_arg] creates a new embedding into Genarg. *) let (wit_proof_instr,globwit_proof_instr,rawwit_proof_instr) = - Genarg.create_arg "proof_instr" + Genarg.create_arg None "proof_instr" let _ = Tacinterp.add_interp_genarg "proof_instr" begin begin fun e x -> (* declares the globalisation function *) |