diff options
Diffstat (limited to 'grammar/q_coqast.ml4')
| -rw-r--r-- | grammar/q_coqast.ml4 | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/grammar/q_coqast.ml4 b/grammar/q_coqast.ml4 index ec1471730..540e78b0b 100644 --- a/grammar/q_coqast.ml4 +++ b/grammar/q_coqast.ml4 @@ -196,6 +196,7 @@ let mlexpr_of_red_expr = function let f = mlexpr_of_list mlexpr_of_occ_constr in <:expr< Genredexpr.Pattern $f l$ >> | Genredexpr.CbvVm o -> <:expr< Genredexpr.CbvVm $mlexpr_of_option mlexpr_of_occ_constr o$ >> + | Genredexpr.CbvNative o -> <:expr< Genredexpr.CbvNative $mlexpr_of_option mlexpr_of_occ_constr o$ >> | Genredexpr.ExtraRedExpr s -> <:expr< Genredexpr.ExtraRedExpr $mlexpr_of_string s$ >> |