From a74d87aca7dd5d09f305be5772b1ee14c926d904 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Tue, 26 Mar 2019 22:09:30 +0100
Subject: [kernel] Don't re-declare scheme side-effects that are already there.

This is an experimental PR as I am not sure I can follow the reasoning
in e1ba72037191b1d4be9de8a0a8fc1faa24eeb12c

Note that in safe_typing we avoid re-declaring effects twice.

This removes a huge number of redeclaration of schemes side-effects
that in fact are already generated such as `eq_ind`.

Anyways we should deprecate the declaration of Schemes on-the-fly, I
don't see the point honestly; just make sure your theory has the right
ones.

Well, going to a more eager declaration scheme could be costly in
terms of size, so OMMV.

TODO: only declare side-effects if the scheme is generated on-the-fly,
add a parameter to the declaration function.
---
 tactics/ind_tables.ml | 5 +----
 1 file changed, 1 insertion(+), 4 deletions(-)

diff --git a/tactics/ind_tables.ml b/tactics/ind_tables.ml
index d1b77f3758..16829482e5 100644
--- a/tactics/ind_tables.ml
+++ b/tactics/ind_tables.ml
@@ -181,10 +181,7 @@ let define_mutual_scheme kind mode names mind =
 
 let find_scheme_on_env_too kind ind =
   let s = String.Map.find kind (Indmap.find ind !scheme_map) in
-  s, Safe_typing.concat_private
-      (Safe_typing.private_con_of_scheme
-            ~kind (Global.safe_env()) [ind, s])
-      Safe_typing.empty_private_constants
+  s, Safe_typing.empty_private_constants
 
 let find_scheme ?(mode=InternalTacticRequest) kind (mind,i as ind) =
   try find_scheme_on_env_too kind ind
-- 
cgit v1.2.3