diff options
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/funind/recdef.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index e742f7b80d..ceea4fa535 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -161,7 +161,7 @@ let rec n_x_id ids n = let simpl_iter clause = reduce (Lazy - {rBeta=true;rIota=true;rZeta= true; rDelta=false; + {rBeta=true;rMatch=true;rFix=true;rCofix=true;rZeta=true;rDelta=false; rConst = [ EvalConstRef (const_of_ref (delayed_force iter_ref))]}) clause |