From 4f5026b1e797e1ed0e501118161052203e1aca50 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 9 Sep 2020 11:09:49 +0200
Subject: Add a fast-path to Tactics.e_change_in_hyps.

In case we give an empty list of occurrences to e_change_in_hyps, we
can return immediately. This saves the allocation of a dummy evar, and
a O(n) map over the context for "local" reduction functions.

Note that passing an empty list of hypotheses is the default for both
the "change" tactic and reduction tactics.
---
 tactics/tactics.ml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 686779b1d2..a607c09010 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -724,7 +724,9 @@ type hyp_conversion =
 | StableHypConv (** Does not introduce new dependencies on variables *)
 | LocalHypConv (** Same as above plus no dependence on the named environment *)
 
-let e_change_in_hyps ~check ~reorder f args =
+let e_change_in_hyps ~check ~reorder f args = match args with
+| [] -> Proofview.tclUNIT ()
+| _ :: _ ->
   Proofview.Goal.enter begin fun gl ->
     let env = Proofview.Goal.env gl in
     let sigma = Tacmach.New.project gl in
-- 
cgit v1.2.3