diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-03-17 15:10:57 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-03-17 15:10:57 +0100 |
| commit | e3e8a4065047e254f5f5c2747227db75f01b7bed (patch) | |
| tree | c7505db28eee92bc1855b6ee0cf275381b4aa106 /plugins/decl_mode/g_decl_mode.ml4 | |
| parent | 22c1e7c3f1d86902b1abf2d887e0e9bf93ddb60d (diff) | |
| parent | 2537e84ba9fa92db6cfd3d7f5e400b1716c31246 (diff) | |
Removing the default value mechanism for generic arguments.
There was a complicated dedicated code in grammar/ to decide whether a generic argument
parsed the empty string. We now only rely on a dynamic decision. This should not affect
efficiency, as it is only made once by declaration of ML tactics.
Diffstat (limited to 'plugins/decl_mode/g_decl_mode.ml4')
| -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 b62cfd6ad..2d096a108 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. *) |