From 724797b1f0e7051a52f30ff0cc432db2cc9345ec Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Mon, 8 Sep 2014 12:52:05 +0200
Subject: Extend the syntax of simpl with a delta flag.

You can write 'simpl -[plus minus] div2'. Simpl does not use it for now.
---
 pretyping/miscops.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'pretyping')

diff --git a/pretyping/miscops.ml b/pretyping/miscops.ml
index 10129306de..9ec031fbb3 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)
-- 
cgit v1.2.3