From a778b72e3ebfbe784fbe55ee5e124ba3f66cfb10 Mon Sep 17 00:00:00 2001 From: ppedrot Date: Fri, 5 Jul 2013 01:49:27 +0000 Subject: Expurgating the useless difference between List0 and List1 at the level of generic arguments. This only matters at parsing time. TODO: the current status is not satisfactory enough, as rule emptyness is still decided w.r.t. generic arguments. This should be done on a grammar entry basis instead. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16617 85f007b7-540e-0410-9357-904b9bb8a0f7 --- tactics/tacintern.ml | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) (limited to 'tactics/tacintern.ml') diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml index 1a63ca2da..d176c516f 100644 --- a/tactics/tacintern.ml +++ b/tactics/tacintern.ml @@ -789,8 +789,7 @@ and intern_genarg ist x = | BindingsArgType -> in_gen (glbwit wit_bindings) (intern_bindings ist (out_gen (rawwit wit_bindings) x)) - | List0ArgType _ -> app_list0 (intern_genarg ist) x - | List1ArgType _ -> app_list1 (intern_genarg ist) x + | ListArgType _ -> app_list (intern_genarg ist) x | OptArgType _ -> app_opt (intern_genarg ist) x | PairArgType _ -> app_pair (intern_genarg ist) (intern_genarg ist) x | ExtraArgType s -> -- cgit v1.2.3