diff options
| author | Enrico Tassi | 2019-04-20 18:42:19 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2019-04-20 18:42:19 +0200 |
| commit | 2e43b09ebd6a4f44f3801290f3205320a21b7b49 (patch) | |
| tree | e86cbf8057e6654a6ca748aea7af1a09a997871d | |
| parent | febcc72ee21d5c874c53a7befd658a93adf103a8 (diff) | |
| parent | a74d87aca7dd5d09f305be5772b1ee14c926d904 (diff) | |
Merge PR #9836: [schemes] Don't re-declare scheme side-effects that are already there.
Reviewed-by: gares
| -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 |