diff options
| author | Arnaud Spiwack | 2014-09-08 12:52:05 +0200 |
|---|---|---|
| committer | Pierre Boutillier | 2014-12-12 16:08:44 +0100 |
| commit | 724797b1f0e7051a52f30ff0cc432db2cc9345ec (patch) | |
| tree | 66038674337785c918a71941d38c19bd62323083 /grammar | |
| parent | a417d138c0a8abc028486c20d59e4f2e82f456ef (diff) | |
Extend the syntax of simpl with a delta flag.
You can write 'simpl -[plus minus] div2'. Simpl does not use it for now.
Diffstat (limited to 'grammar')
| -rw-r--r-- | grammar/q_coqast.ml4 | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/grammar/q_coqast.ml4 b/grammar/q_coqast.ml4 index d6d13375e6..1a11b00282 100644 --- a/grammar/q_coqast.ml4 +++ b/grammar/q_coqast.ml4 @@ -196,7 +196,8 @@ let mlexpr_of_occ_ref_or_constr = let mlexpr_of_red_expr = function | Genredexpr.Red b -> <:expr< Genredexpr.Red $mlexpr_of_bool b$ >> | Genredexpr.Hnf -> <:expr< Genredexpr.Hnf >> - | Genredexpr.Simpl o -> <:expr< Genredexpr.Simpl $mlexpr_of_option mlexpr_of_occ_ref_or_constr o$ >> + | Genredexpr.Simpl (f,o) -> + <:expr< Genredexpr.Simpl $mlexpr_of_red_flags f$ $mlexpr_of_option mlexpr_of_occ_ref_or_constr o$ >> | Genredexpr.Cbv f -> <:expr< Genredexpr.Cbv $mlexpr_of_red_flags f$ >> | Genredexpr.Cbn f -> |