diff options
| author | Maxime Dénès | 2016-07-01 17:24:12 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2016-07-01 17:26:08 +0200 |
| commit | 500d38d0887febb614ddcadebaef81e0c7942584 (patch) | |
| tree | 6ca260dfda3b6d95ff26be24e39010e2c82f881d /plugins/funind | |
| parent | 9501ddd635adea7db07b4df60b8bda1d557dff18 (diff) | |
| parent | 1b09098cc4830f262820d2935a9cd0afa383ed3f (diff) | |
Merge branch 'reduction-flags' into trunk
Was PR#231: Separate flags for fix/cofix/match reduction and clean reduction
function names, itself a revision of PR#117: Isolating flags for cofix/fix
reduction + adjusting names of reduction functions to what they do
Diffstat (limited to 'plugins/funind')
| -rw-r--r-- | plugins/funind/functional_principles_proofs.ml | 2 | ||||
| -rw-r--r-- | plugins/funind/recdef.ml | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index 52094cf085..146749d32b 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -281,7 +281,7 @@ let change_eq env sigma hyp_id (context:Context.Rel.t) x t end_of_type = List.fold_left2 compute_substitution sub args1 args2 end else - if (eq_constr t1 t2) then sub else nochange ~t':(make_refl_eq constructor (Reduction.whd_betadeltaiota env t1) t2) "cannot solve (diff)" + if (eq_constr t1 t2) then sub else nochange ~t':(make_refl_eq constructor (Reduction.whd_all env t1) t2) "cannot solve (diff)" in let sub = compute_substitution Int.Map.empty (snd t1) (snd t2) in let sub = compute_substitution sub (fst t1) (fst t2) in 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 |