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 /toplevel | |
| parent | 92a6a72ec4680d0f241e8b1ddd7b87f7ad11f65e (diff) | |
Removing the registering of default values for generic arguments.
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/g_obligations.ml4 | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/toplevel/g_obligations.ml4 b/toplevel/g_obligations.ml4 index d620febbc1..32ccf21d2b 100644 --- a/toplevel/g_obligations.ml4 +++ b/toplevel/g_obligations.ml4 @@ -32,7 +32,7 @@ let sigref = mkRefC (Qualid (Loc.ghost, Libnames.qualid_of_string "Coq.Init.Spec type 'a withtac_argtype = (Tacexpr.raw_tactic_expr option, 'a) Genarg.abstract_argument_type let wit_withtac : Tacexpr.raw_tactic_expr option Genarg.uniform_genarg_type = - Genarg.create_arg None "withtac" + Genarg.create_arg "withtac" let withtac = Pcoq.create_generic_entry "withtac" (Genarg.rawwit wit_withtac) |