diff options
| author | Pierre-Marie Pédrot | 2020-09-09 11:09:49 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-09-10 14:06:47 +0200 |
| commit | 4f5026b1e797e1ed0e501118161052203e1aca50 (patch) | |
| tree | 927d84249ca1c289bb7ae0f7918020670cc1fbd0 /tactics/tactics.ml | |
| parent | cdfe69d6da6b32338ba74c9f599c74389089c9dd (diff) | |
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.
Diffstat (limited to 'tactics/tactics.ml')
| -rw-r--r-- | tactics/tactics.ml | 4 |
1 files changed, 3 insertions, 1 deletions
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 |