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.
---
 proofs/redexpr.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'proofs/redexpr.ml')

diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml
index 386ad70ecb..c07541335e 100644
--- a/proofs/redexpr.ml
+++ b/proofs/redexpr.ml
@@ -195,7 +195,8 @@ let reduction_of_red_expr env =
       if internal then (e_red try_red_product,DEFAULTcast)
       else (e_red red_product,DEFAULTcast)
   | Hnf -> (e_red hnf_constr,DEFAULTcast)
-  | Simpl o -> (contextualize (if head_style then whd_simpl else simpl) simpl o,DEFAULTcast)
+  | Simpl (_f,o) ->
+     (contextualize (if head_style then whd_simpl else simpl) simpl o,DEFAULTcast)
   | Cbv f -> (e_red (cbv_norm_flags (make_flag f)),DEFAULTcast)
   | Cbn f ->
     let f = strong (fun env evd x -> Stack.zip ~refold:true
-- 
cgit v1.2.3