From 1c10b84c0ce5f96a3afd1fc83c738c76070958c3 Mon Sep 17 00:00:00 2001 From: amblaf Date: Tue, 27 Jun 2017 08:38:20 +0200 Subject: Correcting [build_discriminator] to make the test-suite pass --- tactics/equality.mli | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'tactics/equality.mli') diff --git a/tactics/equality.mli b/tactics/equality.mli index 421f7c7f5..a4d1c0f9b 100644 --- a/tactics/equality.mli +++ b/tactics/equality.mli @@ -126,4 +126,4 @@ val set_eq_dec_scheme_kind : mutual scheme_kind -> unit (* [build_selector env sigma i c t u v] matches on [c] of type [t] and returns [u] in branch [i] and [v] on other branches *) val build_selector : env -> evar_map -> int -> constr -> types -> - constr -> constr -> evar_map * constr + constr -> constr -> constr -- cgit v1.2.3