diff options
| author | ppedrot | 2013-06-12 21:07:49 +0000 |
|---|---|---|
| committer | ppedrot | 2013-06-12 21:07:49 +0000 |
| commit | f3376db665463fa75631f001321a090165c44da1 (patch) | |
| tree | ce836fb16e81228c64a53cc527d4bfac1cdb59d4 /grammar | |
| parent | bea2a4f5fe5cab0abfc27492117c335a311a0c19 (diff) | |
Added Genarg as generic argument type.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16575 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'grammar')
| -rw-r--r-- | grammar/argextend.ml4 | 1 | ||||
| -rw-r--r-- | grammar/q_coqast.ml4 | 1 |
2 files changed, 2 insertions, 0 deletions
diff --git a/grammar/argextend.ml4 b/grammar/argextend.ml4 index e3ee3db404..71ba6b0215 100644 --- a/grammar/argextend.ml4 +++ b/grammar/argextend.ml4 @@ -37,6 +37,7 @@ let rec make_wit loc = function | 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 >> diff --git a/grammar/q_coqast.ml4 b/grammar/q_coqast.ml4 index 6aefd3b720..0f5be6efb7 100644 --- a/grammar/q_coqast.ml4 +++ b/grammar/q_coqast.ml4 @@ -215,6 +215,7 @@ let rec mlexpr_of_argtype loc = function | Genarg.ConstrWithBindingsArgType -> <:expr< Genarg.ConstrWithBindingsArgType >> | Genarg.BindingsArgType -> <:expr< Genarg.BindingsArgType >> | Genarg.RedExprArgType -> <:expr< Genarg.RedExprArgType >> + | Genarg.GenArgType -> <:expr< Genarg.GenArgType >> | Genarg.SortArgType -> <:expr< Genarg.SortArgType >> | Genarg.ConstrArgType -> <:expr< Genarg.ConstrArgType >> | Genarg.ConstrMayEvalArgType -> <:expr< Genarg.ConstrMayEvalArgType >> |