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 /proofs/redexpr.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 'proofs/redexpr.ml')
| -rw-r--r-- | proofs/redexpr.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml index 386ad70ec..c07541335 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 |