From a3ab8b07b912afd1b883ed60bd532b5a29bccd8f Mon Sep 17 00:00:00 2001 From: letouzey Date: Tue, 29 May 2012 11:09:01 +0000 Subject: 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 --- parsing/g_constr.ml4 | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'parsing/g_constr.ml4') 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' -- cgit v1.2.3