diff options
| -rw-r--r-- | dev/base_include | 7 | ||||
| -rw-r--r-- | dev/printers.mllib | 2 | ||||
| -rw-r--r-- | parsing/egrammar.ml | 7 | ||||
| -rw-r--r-- | parsing/g_constr.ml4 | 15 | ||||
| -rw-r--r-- | parsing/grammar.mllib | 45 |
5 files changed, 26 insertions, 50 deletions
diff --git a/dev/base_include b/dev/base_include index 38a5972e9..a0c4928f6 100644 --- a/dev/base_include +++ b/dev/base_include @@ -13,6 +13,7 @@ #directory "proofs";; #directory "tactics";; #directory "translate";; +#directory "intf";; #directory "+camlp4";; (* lazy solution: add both of camlp4/5 so that *) #directory "+camlp5";; (* Gramext is found in top_printers.ml *) @@ -68,6 +69,7 @@ open Library open Cases open Pattern +open Patternops open Cbv open Classops open Pretyping @@ -76,6 +78,7 @@ open Classops open Clenv open Clenvtac open Glob_term +open Glob_ops open Coercion open Recordops open Detyping @@ -102,7 +105,11 @@ open Notation open Ppextend open Reserve open Syntax_def +open Constrexpr +open Constrexpr_ops open Topconstr +open Notation_term +open Notation_ops open Prettyp open Search diff --git a/dev/printers.mllib b/dev/printers.mllib index a5e0d27be..955eb3650 100644 --- a/dev/printers.mllib +++ b/dev/printers.mllib @@ -105,6 +105,8 @@ Tok Lexer Ppextend Genarg +Constrexpr_ops +Notation_ops Topconstr Notation Dumpglob diff --git a/parsing/egrammar.ml b/parsing/egrammar.ml index d55363b17..b0c705400 100644 --- a/parsing/egrammar.ml +++ b/parsing/egrammar.ml @@ -108,8 +108,13 @@ let make_constr_action in make ([],[],[]) (List.rev pil) +(* TODO: factorize the error message with error_invalid_pattern_notaition + without introducing useless dependencies *) + let check_cases_pattern_env loc (env,envlist,hasbinders) = - if hasbinders then Topconstr.error_invalid_pattern_notation loc else (env,envlist) + if hasbinders then + Errors.user_err_loc (loc,"",str "Invalid notation for pattern.") + else (env,envlist) let make_cases_pattern_action (f : loc -> cases_pattern_notation_substitution -> cases_pattern_expr) pil = diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4 index c62039739..ca462a702 100644 --- a/parsing/g_constr.ml4 +++ b/parsing/g_constr.ml4 @@ -7,10 +7,6 @@ (************************************************************************) open Pp -open Pcoq -open Constr -open Prim -open Glob_term open Term open Names open Libnames @@ -22,6 +18,13 @@ open Compat open Misctypes open Decl_kinds +open Pcoq +open Pcoq.Prim +open Pcoq.Constr + +(* TODO: avoid this redefinition without an extra dep to Notation_ops *) +let ldots_var = id_of_string ".." + let constr_kw = [ "forall"; "fun"; "match"; "fix"; "cofix"; "with"; "in"; "for"; "end"; "as"; "let"; "if"; "then"; "else"; "return"; @@ -184,7 +187,7 @@ GEXTEND Gram CApp(loc,(None,CPatVar(locid,(true,id))),args) ] | "9" [ ".."; c = operconstr LEVEL "0"; ".." -> - CAppExpl (loc,(None,Ident (loc,Notation_ops.ldots_var)),[c]) ] + CAppExpl (loc,(None,Ident (loc,ldots_var)),[c]) ] | "8" [ ] | "1" LEFTA [ c=operconstr; ".("; f=global; args=LIST0 appl_arg; ")" -> @@ -396,7 +399,7 @@ GEXTEND Gram | id = name; idl = LIST0 name; bl = binders -> binders_of_names (id::idl) @ bl | id1 = name; ".."; id2 = name -> - [LocalRawAssum ([id1;(loc,Name Notation_ops.ldots_var);id2], + [LocalRawAssum ([id1;(loc,Name 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 db0c20bef..226ef4b36 100644 --- a/parsing/grammar.mllib +++ b/parsing/grammar.mllib @@ -13,9 +13,7 @@ Bigint Dyn Hashcons Predicate -Rtree Option -Store Hashtbl_alt Names @@ -23,51 +21,10 @@ Univ Esubst Term Mod_subst -Sign -Cbytecodes -Copcodes -Cemitcodes -Declarations -Retroknowledge -Pre_env -Cbytegen -Environ -Conv_oracle -Closure -Reduction -Type_errors -Entries -Modops -Inductive -Typeops -Indtypes -Cooking -Term_typing -Subtyping -Mod_typing -Safe_typing Nameops Libnames Summary -Nametab -Libobject -Lib -Goptions -Decl_kinds -Global -Locusops -Termops -Namegen -Evd -Reductionops -Inductiveops -Miscops -Glob_ops -Detyping -Notation_ops -Constrexpr_ops -Topconstr Genarg Ppextend Tok @@ -84,6 +41,8 @@ Tacextend Vernacextend Redops +Constrexpr_ops +Locusops G_prim G_tactic G_ltac |