diff options
| author | Pierre-Marie Pédrot | 2016-03-17 14:42:51 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-03-17 14:51:20 +0100 |
| commit | 2537e84ba9fa92db6cfd3d7f5e400b1716c31246 (patch) | |
| tree | c7505db28eee92bc1855b6ee0cf275381b4aa106 /plugins/decl_mode | |
| parent | 92a6a72ec4680d0f241e8b1ddd7b87f7ad11f65e (diff) | |
Removing the registering of default values for generic arguments.
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 b62cfd6add..2d096a1081 100644 --- a/plugins/decl_mode/g_decl_mode.ml4 +++ b/plugins/decl_mode/g_decl_mode.ml4 @@ -87,7 +87,7 @@ let vernac_proof_instr instr = (* Only declared at raw level, because only used in vernac commands. *) let wit_proof_instr : (raw_proof_instr, glob_proof_instr, proof_instr) Genarg.genarg_type = - Genarg.make0 None "proof_instr" + Genarg.make0 "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. *) |