diff options
| author |  Arnaud Spiwack <arnaud@spiwack.net> | 2014-09-08 12:52:05 +0200 |
|---|---|---|
| committer |  Pierre Boutillier <pierre.boutillier@pps.univ-paris-diderot.fr> | 2014-12-12 16:08:44 +0100 |
| commit | 724797b1f0e7051a52f30ff0cc432db2cc9345ec (patch) | |
| tree | 66038674337785c918a71941d38c19bd62323083 /pretyping/miscops.ml | |
| 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 'pretyping/miscops.ml')
| -rw-r--r-- | pretyping/miscops.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/pretyping/miscops.ml b/pretyping/miscops.ml index 10129306d..9ec031fbb 100644 --- a/pretyping/miscops.ml +++ b/pretyping/miscops.ml @@ -49,7 +49,8 @@ let map_occs f (occ,e) = (occ,f e) let map_red_expr_gen f g h = function | Fold l -> Fold (List.map f l) | Pattern occs_l -> Pattern (List.map (map_occs f) occs_l) - | Simpl occs_o -> Simpl (Option.map (map_occs (map_union g h)) occs_o) + | Simpl (flags,occs_o) -> + Simpl (map_flags g flags, Option.map (map_occs (map_union g h)) occs_o) | Unfold occs_l -> Unfold (List.map (map_occs g) occs_l) | Cbv flags -> Cbv (map_flags g flags) | Lazy flags -> Lazy (map_flags g flags) |