From 724797b1f0e7051a52f30ff0cc432db2cc9345ec Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack <arnaud@spiwack.net>
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.
---
 intf/genredexpr.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'intf')

diff --git a/intf/genredexpr.mli b/intf/genredexpr.mli
index a59278bb0..a9fc47348 100644
--- a/intf/genredexpr.mli
+++ b/intf/genredexpr.mli
@@ -32,7 +32,7 @@ type 'a glob_red_flag = {
 type ('a,'b,'c) red_expr_gen =
   | Red of bool
   | Hnf
-  | Simpl of ('b,'c) Util.union Locus.with_occurrences option
+  | Simpl of 'b glob_red_flag*('b,'c) Util.union Locus.with_occurrences option
   | Cbv of 'b glob_red_flag
   | Cbn of 'b glob_red_flag
   | Lazy of 'b glob_red_flag
-- 
cgit v1.2.3