diff options
| -rw-r--r-- | tactics/autorewrite.ml | 38 |
1 files changed, 16 insertions, 22 deletions
diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml index 785cc011f4..cc56de066d 100644 --- a/tactics/autorewrite.ml +++ b/tactics/autorewrite.ml @@ -212,38 +212,32 @@ let inHintRewrite : string * HintDN.t -> Libobject.obj = ~cache:cache_hintrewrite ~subst:(Some subst_hintrewrite) -open Clenv - type hypinfo = { - hyp_ty : types; - hyp_left : constr; - hyp_right : constr; + hyp_ty : EConstr.types; + hyp_pat : EConstr.constr; } let decompose_applied_relation env sigma c ctype left2right = let find_rel ty = - let eqclause = Clenv.mk_clenv_from_env env sigma None (EConstr.of_constr c,ty) in - let eqclause = fst (clenv_pose_metas_as_evars eqclause (Evd.undefined_metas eqclause.evd)) in - let (_, args) = Termops.decompose_app_vect sigma (Clenv.clenv_type eqclause) in + (* FIXME: this is nonsense, we generate evars and then we drop the + corresponding evarmap. This sometimes works because [Term_dnet] performs + evar surgery via [Termops.filtering]. *) + let sigma, ty = Clenv.make_evar_clause env sigma ty in + let (_, args) = Termops.decompose_app_vect sigma ty.Clenv.cl_concl in let len = Array.length args in if 2 <= len then - let c1 = args.(len - 2) in - let c2 = args.(len - 1) in - let _ty1, _ty2 = Retyping.get_type_of env eqclause.evd c1, Retyping.get_type_of env eqclause.evd c2 in - (* XXX: It looks like mk_clenv_from_env should be fixed instead? *) - let open EConstr in - let hyp_ty = Unsafe.to_constr ty in - let hyp_left = Unsafe.to_constr @@ c1 in - let hyp_right = Unsafe.to_constr @@ c2 in - Some { hyp_ty; hyp_left; hyp_right; } + let c1 = args.(len - 2) in + let c2 = args.(len - 1) in + Some (if left2right then c1 else c2) else None in match find_rel ctype with - | Some c -> Some c + | Some c -> Some { hyp_pat = c; hyp_ty = ctype } | None -> let ctx,t' = Reductionops.splay_prod_assum env sigma ctype in (* Search for underlying eq *) - match find_rel (it_mkProd_or_LetIn t' ctx) with - | Some c -> Some c + let ctype = it_mkProd_or_LetIn t' ctx in + match find_rel ctype with + | Some c -> Some { hyp_pat = c; hyp_ty = ctype } | None -> None let find_applied_relation ?loc env sigma c left2right = @@ -267,8 +261,8 @@ let add_rew_rules base lrul = (fun dn {CAst.loc;v=((c,ctx),b,t)} -> let sigma = Evd.merge_context_set Evd.univ_rigid sigma ctx in let info = find_applied_relation ?loc env sigma c b in - let pat = if b then info.hyp_left else info.hyp_right in - let rul = { rew_lemma = c; rew_type = info.hyp_ty; + let pat = EConstr.Unsafe.to_constr info.hyp_pat in + let rul = { rew_lemma = c; rew_type = EConstr.Unsafe.to_constr info.hyp_ty; rew_pat = pat; rew_ctx = ctx; rew_l2r = b; rew_tac = Option.map intern t} in incr counter; |