diff options
| author | ppedrot | 2013-06-21 12:36:19 +0000 |
|---|---|---|
| committer | ppedrot | 2013-06-21 12:36:19 +0000 |
| commit | 9024a91b59b9ecfb94e68b3748f2a9a66adcf515 (patch) | |
| tree | 44d3483d8ec18b2f8bba7a0a348632edbfad465c /grammar | |
| parent | 47cbc272e79db52cc96dfe3d4d1cd4b978e4fa2a (diff) | |
Cutting the dependency of Genarg in constr_expr, glob_constr
related types. This will ultimately allow putting genargs into
these ASTs.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16600 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'grammar')
| -rw-r--r-- | grammar/argextend.ml4 | 28 | ||||
| -rw-r--r-- | grammar/grammar.mllib | 1 |
2 files changed, 15 insertions, 14 deletions
diff --git a/grammar/argextend.ml4 b/grammar/argextend.ml4 index 6fde4fafeb..dffca2c622 100644 --- a/grammar/argextend.ml4 +++ b/grammar/argextend.ml4 @@ -33,20 +33,20 @@ let mk_extraarg s = qualified_name ("Extrawit.wit_" ^ s) let rec make_wit loc = function - | IntOrVarArgType -> <:expr< Genarg.wit_int_or_var >> - | IntroPatternArgType -> <:expr< Genarg.wit_intro_pattern >> - | IdentArgType b -> <:expr< Genarg.wit_ident_gen $mlexpr_of_bool b$ >> - | VarArgType -> <:expr< Genarg.wit_var >> - | RefArgType -> <:expr< Genarg.wit_ref >> - | QuantHypArgType -> <:expr< Genarg.wit_quant_hyp >> - | GenArgType -> <:expr< Genarg.wit_genarg >> - | SortArgType -> <:expr< Genarg.wit_sort >> - | ConstrArgType -> <:expr< Genarg.wit_constr >> - | ConstrMayEvalArgType -> <:expr< Genarg.wit_constr_may_eval >> - | RedExprArgType -> <:expr< Genarg.wit_red_expr >> - | OpenConstrArgType b -> <:expr< Genarg.wit_open_constr_gen $mlexpr_of_bool b$ >> - | ConstrWithBindingsArgType -> <:expr< Genarg.wit_constr_with_bindings >> - | BindingsArgType -> <:expr< Genarg.wit_bindings >> + | IntOrVarArgType -> <:expr< Constrarg.wit_int_or_var >> + | IntroPatternArgType -> <:expr< Constrarg.wit_intro_pattern >> + | IdentArgType b -> <:expr< Constrarg.wit_ident_gen $mlexpr_of_bool b$ >> + | VarArgType -> <:expr< Constrarg.wit_var >> + | RefArgType -> <:expr< Constrarg.wit_ref >> + | QuantHypArgType -> <:expr< Constrarg.wit_quant_hyp >> + | GenArgType -> <:expr< Constrarg.wit_genarg >> + | SortArgType -> <:expr< Constrarg.wit_sort >> + | ConstrArgType -> <:expr< Constrarg.wit_constr >> + | ConstrMayEvalArgType -> <:expr< Constrarg.wit_constr_may_eval >> + | RedExprArgType -> <:expr< Constrarg.wit_red_expr >> + | OpenConstrArgType b -> <:expr< Constrarg.wit_open_constr_gen $mlexpr_of_bool b$ >> + | ConstrWithBindingsArgType -> <:expr< Constrarg.wit_constr_with_bindings >> + | BindingsArgType -> <:expr< Constrarg.wit_bindings >> | List0ArgType t -> <:expr< Genarg.wit_list0 $make_wit loc t$ >> | List1ArgType t -> <:expr< Genarg.wit_list1 $make_wit loc t$ >> | OptArgType t -> <:expr< Genarg.wit_opt $make_wit loc t$ >> diff --git a/grammar/grammar.mllib b/grammar/grammar.mllib index a97b8a2a63..f361bee492 100644 --- a/grammar/grammar.mllib +++ b/grammar/grammar.mllib @@ -28,6 +28,7 @@ Names Libnames Genarg Stdarg +Constrarg Tok Lexer Extrawit |