diff options
| -rw-r--r-- | kernel/reduction.ml | 20 | ||||
| -rw-r--r-- | tactics/eqschemes.ml | 5 |
2 files changed, 14 insertions, 11 deletions
diff --git a/kernel/reduction.ml b/kernel/reduction.ml index 2f11f3dd6b..11ece78fe0 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -315,11 +315,19 @@ type conv_tab = { let push_relevance infos r = { infos with relevances = r.Context.binder_relevance :: infos.relevances } -let rec skip_pattern infos n c1 c2 = - if Int.equal n 0 then infos, c1, c2 +let push_relevances infos nas = + { infos with relevances = Array.fold_left (fun l x -> x.Context.binder_relevance :: l) infos.relevances nas } + +let rec skip_pattern infos relevances n c1 c2 = + if Int.equal n 0 then {infos with relevances}, c1, c2 else match kind c1, kind c2 with - | Lambda (x, _, c1), Lambda (_, _, c2) -> skip_pattern (push_relevance infos x) (pred n) c1 c2 - | _ -> raise IrregularPatternShape + | Lambda (x, _, c1), Lambda (_, _, c2) -> + skip_pattern infos (x.Context.binder_relevance :: relevances) (pred n) c1 c2 + | _ -> raise IrregularPatternShape + +let skip_pattern infos n c1 c2 = + if Int.equal n 0 then infos, c1, c2 + else skip_pattern infos infos.relevances n c1 c2 let is_irrelevant infos lft c = let env = info_env infos.cnv_inf in @@ -589,7 +597,7 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = let el2 = el_stack lft2 v2 in let cuniv = convert_vect l2r infos el1 el2 fty1 fty2 cuniv in let cuniv = - let infos = Array.fold_left push_relevance infos na1 in + let infos = push_relevances infos na1 in convert_vect l2r infos (el_liftn n el1) (el_liftn n el2) fcl1 fcl2 cuniv in @@ -608,7 +616,7 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = let el2 = el_stack lft2 v2 in let cuniv = convert_vect l2r infos el1 el2 fty1 fty2 cuniv in let cuniv = - let infos = Array.fold_left push_relevance infos na1 in + let infos = push_relevances infos na1 in convert_vect l2r infos (el_liftn n el1) (el_liftn n el2) fcl1 fcl2 cuniv in diff --git a/tactics/eqschemes.ml b/tactics/eqschemes.ml index 073d66e4aa..3fdd97616f 100644 --- a/tactics/eqschemes.ml +++ b/tactics/eqschemes.ml @@ -686,11 +686,6 @@ let build_r2l_rew_scheme dep env ind k = let (sigma, c) = build_case_analysis_scheme env sigma indu dep k in c, Evd.evar_universe_context sigma -let build_l2r_rew_scheme = build_l2r_rew_scheme -let build_l2r_forward_rew_scheme = build_l2r_forward_rew_scheme -let build_r2l_rew_scheme = build_r2l_rew_scheme -let build_r2l_forward_rew_scheme = build_r2l_forward_rew_scheme - (**********************************************************************) (* Register the rewriting schemes *) (**********************************************************************) |