From a9b76df171ceea443885bb4be919ea586a82beee Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 20 Jan 2017 10:55:17 +0100
Subject: Do not add redundant side effects in tactic code.

This was observable in long proofs, because side effects kept being
duplicated, leading to an additional cost linear in the size of the proof.
This commit touches kernel files, but the corresponding API is only used
in tactic-facing code so that the side_effects type remains opaque. Thus
it does not affect the kernel safety.
---
 kernel/term_typing.mli | 1 +
 1 file changed, 1 insertion(+)

(limited to 'kernel/term_typing.mli')

diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli
index fcd95576c0..89b5fc40e3 100644
--- a/kernel/term_typing.mli
+++ b/kernel/term_typing.mli
@@ -30,6 +30,7 @@ val inline_entry_side_effects :
     yet type checked proof. *)
 
 val uniq_seff : side_effects -> side_effects
+val equal_eff : side_effect -> side_effect -> bool
 
 val translate_constant :
   structure_body -> env -> constant -> side_effects constant_entry ->
-- 
cgit v1.2.3