diff options
| author |  ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-07-05 01:49:27 +0000 |
|---|---|---|
| committer | ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-07-05 01:49:27 +0000 |
| commit | a778b72e3ebfbe784fbe55ee5e124ba3f66cfb10 (patch) | |
| tree | 45ccc4afcf8edc5aed09d76b45c826a1e779af66 /parsing | |
| parent | 556c2ce6f1b09d09484cc83f6ada213496add45b (diff) | |
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
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/pcoq.ml4 | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4 index 211bf2632..d74de5ac6 100644 --- a/parsing/pcoq.ml4 +++ b/parsing/pcoq.ml4 @@ -768,23 +768,23 @@ let rec interp_entry_name static up_level s sep = let l = String.length s in if l > 8 && coincide s "ne_" 0 && coincide s "_list" (l - 5) then let t, g = interp_entry_name static up_level (String.sub s 3 (l-8)) "" in - List1ArgType t, Alist1 g + ListArgType t, Alist1 g else if l > 12 && coincide s "ne_" 0 && coincide s "_list_sep" (l-9) then let t, g = interp_entry_name static up_level (String.sub s 3 (l-12)) "" in - List1ArgType t, Alist1sep (g,sep) + ListArgType t, Alist1sep (g,sep) else if l > 5 && coincide s "_list" (l-5) then let t, g = interp_entry_name static up_level (String.sub s 0 (l-5)) "" in - List0ArgType t, Alist0 g + ListArgType t, Alist0 g else if l > 9 && coincide s "_list_sep" (l-9) then let t, g = interp_entry_name static up_level (String.sub s 0 (l-9)) "" in - List0ArgType t, Alist0sep (g,sep) + ListArgType t, Alist0sep (g,sep) else if l > 4 && coincide s "_opt" (l-4) then let t, g = interp_entry_name static up_level (String.sub s 0 (l-4)) "" in OptArgType t, Aopt g else if l > 5 && coincide s "_mods" (l-5) then let t, g = interp_entry_name static up_level (String.sub s 0 (l-1)) "" in - List0ArgType t, Amodifiers g + ListArgType t, Amodifiers g else let s = match s with "hyp" -> "var" | _ -> s in let check_lvl n = match up_level with |