From 61dc740ed1c3780cccaec00d059a28f0d31d0052 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Mon, 4 Jun 2012 12:07:52 +0200 Subject: Imported Upstream version 8.4~gamma0+really8.4beta2 --- plugins/subtac/g_subtac.ml4 | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'plugins/subtac/g_subtac.ml4') 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 ] -- cgit v1.2.3