diff options
Diffstat (limited to 'tactics/autorewrite.ml')
| -rw-r--r-- | tactics/autorewrite.ml | 26 |
1 files changed, 14 insertions, 12 deletions
diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml index c3857e6b..c8fd0b7a 100644 --- a/tactics/autorewrite.ml +++ b/tactics/autorewrite.ml @@ -30,7 +30,7 @@ let subst_hint subst hint = let cst' = subst_mps subst hint.rew_lemma in let typ' = subst_mps subst hint.rew_type in let pat' = subst_mps subst hint.rew_pat in - let t' = Option.smartmap (Genintern.generic_substitute subst) hint.rew_tac in + let t' = Option.Smart.map (Genintern.generic_substitute subst) hint.rew_tac in if hint.rew_lemma == cst' && hint.rew_type == typ' && hint.rew_tac == t' then hint else { hint with rew_lemma = cst'; rew_type = typ'; @@ -93,7 +93,7 @@ let one_base general_rewrite_maybe_in tac_main bas = let try_rewrite dir ctx c tc = Proofview.Goal.enter begin fun gl -> let sigma = Proofview.Goal.sigma gl in - let subst, ctx' = Universes.fresh_universe_context_set_instance ctx in + let subst, ctx' = UnivGen.fresh_universe_context_set_instance ctx in let c' = Vars.subst_univs_level_constr subst c in let sigma = Evd.merge_context_set Evd.univ_flexible sigma ctx' in Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma) @@ -228,7 +228,7 @@ let decompose_applied_relation metas env sigma c ctype left2right = if metas then eqclause else clenv_pose_metas_as_evars eqclause (Evd.undefined_metas eqclause.evd) in - let (equiv, args) = decompose_app (EConstr.Unsafe.to_constr (Clenv.clenv_type eqclause)) in + let (equiv, args) = EConstr.decompose_app sigma (Clenv.clenv_type eqclause) in let rec split_last_two = function | [c1;c2] -> [],(c1, c2) | x::y::z -> @@ -236,17 +236,19 @@ let decompose_applied_relation metas env sigma c ctype left2right = | _ -> raise Not_found in try - let others,(c1,c2) = split_last_two args in - let ty1, ty2 = - Typing.unsafe_type_of env eqclause.evd (EConstr.of_constr c1), Typing.unsafe_type_of env eqclause.evd (EConstr.of_constr c2) - in - let ty = EConstr.Unsafe.to_constr ty in - let ty1 = EConstr.Unsafe.to_constr ty1 in + let others,(c1,c2) = split_last_two args in + let ty1, ty2 = Typing.unsafe_type_of env eqclause.evd c1, Typing.unsafe_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_car = Unsafe.to_constr ty1 in + let hyp_prf = Unsafe.to_constr @@ Clenv.clenv_value eqclause in + let hyp_rel = Unsafe.to_constr @@ mkApp (equiv, Array.of_list others) in + let hyp_left = Unsafe.to_constr @@ c1 in + let hyp_right = Unsafe.to_constr @@ c2 in (* if not (evd_convertible env eqclause.evd ty1 ty2) then None *) (* else *) - Some { hyp_cl=eqclause; hyp_prf=EConstr.Unsafe.to_constr (Clenv.clenv_value eqclause); hyp_ty = ty; - hyp_car=ty1; hyp_rel=mkApp (equiv, Array.of_list others); - hyp_l2r=left2right; hyp_left=c1; hyp_right=c2; } + Some { hyp_cl=eqclause; hyp_prf; hyp_ty; hyp_car; hyp_rel; hyp_l2r=left2right; hyp_left; hyp_right; } with Not_found -> None in match find_rel ctype with |