diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-05-29 11:09:01 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-05-29 11:09:01 +0000 |
| commit | a3ab8b07b912afd1b883ed60bd532b5a29bccd8f (patch) | |
| tree | 8f5755d4bca03047baa9cebf41d8157b0380d92c /parsing/g_constr.ml4 | |
| parent | 525090840aa3cd661bdac013860766fcc3886731 (diff) | |
Stuff about notation_constr (ex-aconstr) now in notation_ops.ml
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15381 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing/g_constr.ml4')
| -rw-r--r-- | parsing/g_constr.ml4 | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4 index 1bc46f83f..3e1af6fed 100644 --- a/parsing/g_constr.ml4 +++ b/parsing/g_constr.ml4 @@ -183,7 +183,7 @@ GEXTEND Gram CApp(loc,(None,CPatVar(locid,(true,id))),args) ] | "9" [ ".."; c = operconstr LEVEL "0"; ".." -> - CAppExpl (loc,(None,Ident (loc,Topconstr.ldots_var)),[c]) ] + CAppExpl (loc,(None,Ident (loc,Notation_ops.ldots_var)),[c]) ] | "8" [ ] | "1" LEFTA [ c=operconstr; ".("; f=global; args=LIST0 appl_arg; ")" -> @@ -395,7 +395,7 @@ GEXTEND Gram | id = name; idl = LIST0 name; bl = binders -> binders_of_names (id::idl) @ bl | id1 = name; ".."; id2 = name -> - [LocalRawAssum ([id1;(loc,Name Topconstr.ldots_var);id2], + [LocalRawAssum ([id1;(loc,Name Notation_ops.ldots_var);id2], Default Explicit,CHole (loc,None))] | bl = closed_binder; bl' = binders -> bl@bl' |