diff options
| author | Pierre-Marie Pédrot | 2016-03-17 15:10:57 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-03-17 15:10:57 +0100 |
| commit | e3e8a4065047e254f5f5c2747227db75f01b7bed (patch) | |
| tree | c7505db28eee92bc1855b6ee0cf275381b4aa106 /plugins/funind | |
| 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/funind')
| -rw-r--r-- | plugins/funind/g_indfun.ml4 | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4 index 97b9e95e10..61ada5cc8c 100644 --- a/plugins/funind/g_indfun.ml4 +++ b/plugins/funind/g_indfun.ml4 @@ -146,7 +146,7 @@ module Tactic = Pcoq.Tactic type function_rec_definition_loc_argtype = (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) Loc.located let (wit_function_rec_definition_loc : function_rec_definition_loc_argtype Genarg.uniform_genarg_type) = - Genarg.create_arg None "function_rec_definition_loc" + Genarg.create_arg "function_rec_definition_loc" let function_rec_definition_loc = Pcoq.create_generic_entry "function_rec_definition_loc" (Genarg.rawwit wit_function_rec_definition_loc) |