diff options
author | Stephane Glondu <steph@glondu.net> | 2012-06-04 12:07:52 +0200 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2012-06-04 12:07:52 +0200 |
commit | 61dc740ed1c3780cccaec00d059a28f0d31d0052 (patch) | |
tree | d88d05baf35b9b09a034233300f35a694f9fa6c2 /plugins/subtac/g_subtac.ml4 | |
parent | 97fefe1fcca363a1317e066e7f4b99b9c1e9987b (diff) |
Imported Upstream version 8.4~gamma0+really8.4beta2upstream/8.4_gamma0+really8.4beta2
Diffstat (limited to 'plugins/subtac/g_subtac.ml4')
-rw-r--r-- | plugins/subtac/g_subtac.ml4 | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/plugins/subtac/g_subtac.ml4 b/plugins/subtac/g_subtac.ml4 index ca1240e5..6a131d39 100644 --- a/plugins/subtac/g_subtac.ml4 +++ b/plugins/subtac/g_subtac.ml4 @@ -75,14 +75,14 @@ type 'a gallina_loc_argtype = (Vernacexpr.vernac_expr located, 'a) Genarg.abstra let (wit_subtac_gallina_loc : Genarg.tlevel gallina_loc_argtype), (globwit_subtac_gallina_loc : Genarg.glevel gallina_loc_argtype), (rawwit_subtac_gallina_loc : Genarg.rlevel gallina_loc_argtype) = - Genarg.create_arg "subtac_gallina_loc" + Genarg.create_arg None "subtac_gallina_loc" type 'a withtac_argtype = (Tacexpr.raw_tactic_expr option, 'a) Genarg.abstract_argument_type let (wit_subtac_withtac : Genarg.tlevel withtac_argtype), (globwit_subtac_withtac : Genarg.glevel withtac_argtype), (rawwit_subtac_withtac : Genarg.rlevel withtac_argtype) = - Genarg.create_arg "subtac_withtac" + Genarg.create_arg None "subtac_withtac" VERNAC COMMAND EXTEND Subtac [ "Program" subtac_gallina_loc(g) ] -> [ Subtac.subtac g ] |