diff options
| author | Emilio Jesus Gallego Arias | 2019-03-26 22:09:30 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-03-26 22:15:30 +0100 |
| commit | a74d87aca7dd5d09f305be5772b1ee14c926d904 (patch) | |
| tree | 07cfc71c364b333861a8dd41e65ddd58f57fa444 | |
| parent | 2ac275c0f3e65a402951de86a61c77dd0e0782f8 (diff) | |
[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.
| -rw-r--r-- | tactics/ind_tables.ml | 5 |
1 files changed, 1 insertions, 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 |