From 369077bec1c84bc7faa1f5630aac2e51f13bc644 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Pierre-Marie=20P=C3=A9drot?= Date: Wed, 26 Oct 2022 13:45:08 +0200 Subject: [PATCH] Fast path in the Tacticals.check_evars function. We only care about the difference between undefined evars, so whenever the new evarmap has physically the same undefined evars as the original one, we return immediately. This seriously alleviates the slowdowns introduced in #17564. --- tactics/tacticals.ml | 3 +++ 1 file changed, 3 insertions(+) diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index 9be8614bd111..d4ed359d7008 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -379,6 +379,7 @@ let tclPROGRESS t = (* Check that holes in arguments have been resolved *) let check_evars env sigma extsigma origsigma = + (* origsigma ⊆ extsigma ⊆ sigma *) let reachable = lazy (Evarutil.reachable_from_evars sigma (Evar.Map.domain (Evd.undefined_map origsigma))) in let rec is_undefined_up_to_restriction sigma evk = @@ -393,6 +394,8 @@ let check_evars env sigma extsigma origsigma = evar remaining after typing from the initial term given to apply/elim and co tactics, is it correct? *) None in + if Evd.undefined_map extsigma == Evd.undefined_map origsigma then () + else let rest = Evd.fold_undefined (fun evk evi acc -> match is_undefined_up_to_restriction sigma evk with