diff options
Diffstat (limited to 'tactics/ind_tables.ml')
| -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 |