diff options
| author | letouzey | 2012-05-29 11:09:01 +0000 |
|---|---|---|
| committer | letouzey | 2012-05-29 11:09:01 +0000 |
| commit | a3ab8b07b912afd1b883ed60bd532b5a29bccd8f (patch) | |
| tree | 8f5755d4bca03047baa9cebf41d8157b0380d92c /parsing | |
| 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')
| -rw-r--r-- | parsing/g_constr.ml4 | 4 | ||||
| -rw-r--r-- | parsing/grammar.mllib | 1 | ||||
| -rw-r--r-- | parsing/ppconstr.ml | 2 | ||||
| -rw-r--r-- | parsing/prettyp.ml | 2 |
4 files changed, 5 insertions, 4 deletions
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4 index 1bc46f83f7..3e1af6fed7 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' diff --git a/parsing/grammar.mllib b/parsing/grammar.mllib index 1a9c03f723..182234f7cf 100644 --- a/parsing/grammar.mllib +++ b/parsing/grammar.mllib @@ -65,6 +65,7 @@ Inductiveops Miscops Glob_ops Detyping +Notation_ops Topconstr Genarg Ppextend diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml index d7e968ad42..1fc7217694 100644 --- a/parsing/ppconstr.ml +++ b/parsing/ppconstr.ml @@ -467,7 +467,7 @@ let pr pr sep inherited a = p, lproj | CAppExpl (_,(None,Ident (_,var)),[t]) | CApp (_,(_,CRef(Ident(_,var))),[t,None]) - when var = Topconstr.ldots_var -> + when var = Notation_ops.ldots_var -> hov 0 (str ".." ++ pr spc (latom,E) t ++ spc () ++ str ".."), larg | CAppExpl (_,(None,f),l) -> pr_appexpl (pr mt) f l, lapp | CApp (_,(Some i,f),l) -> diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml index d90e655b14..f1f6db64d1 100644 --- a/parsing/prettyp.ml +++ b/parsing/prettyp.ml @@ -435,7 +435,7 @@ let gallina_print_constant_with_infos sp = let gallina_print_syntactic_def kn = let qid = Nametab.shortest_qualid_of_syndef Idset.empty kn and (vars,a) = Syntax_def.search_syntactic_definition kn in - let c = Topconstr.glob_constr_of_notation_constr dummy_loc a in + let c = Notation_ops.glob_constr_of_notation_constr dummy_loc a in hov 2 (hov 4 (str "Notation " ++ pr_qualid qid ++ |