From 671e5ad1795b2606a5da9c65758fb0d337c4d14e Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Mon, 13 Mar 2017 23:06:33 +0100 Subject: Attempt to improve error message when "apply in" fail. - Adding a better location in the "apply" on the fly pattern. - Printing statement of lemma and of hypothesis. Was suggested by discussion at wish report #5390. --- intf/misctypes.mli | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'intf') diff --git a/intf/misctypes.mli b/intf/misctypes.mli index e4f595ac4..33dc2a335 100644 --- a/intf/misctypes.mli +++ b/intf/misctypes.mli @@ -28,7 +28,7 @@ and 'constr intro_pattern_action_expr = | IntroWildcard | IntroOrAndPattern of 'constr or_and_intro_pattern_expr | IntroInjection of (Loc.t * 'constr intro_pattern_expr) list - | IntroApplyOn of 'constr * (Loc.t * 'constr intro_pattern_expr) + | IntroApplyOn of (Loc.t * 'constr) * (Loc.t * 'constr intro_pattern_expr) | IntroRewrite of bool and 'constr or_and_intro_pattern_expr = | IntroOrPattern of (Loc.t * 'constr intro_pattern_expr) list list -- cgit v1.2.3