diff options
| author | Pierre-Marie Pédrot | 2019-12-10 09:44:08 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-12-10 10:53:54 +0100 |
| commit | 5ccf803a86bc46d67038f4d33d26d5c9e899027f (patch) | |
| tree | 45fc5c34c1054ad7c5cf7989642911b784217223 /tactics/ind_tables.ml | |
| parent | 50221b84f6af681f69e8f9847a851329a4662509 (diff) | |
Side-effect free wrapper around already declared schemes.
Some calls are actually guarded by a check that the scheme is already in
the cache. There is no reason to generate dummy side-effects in that case.
Diffstat (limited to 'tactics/ind_tables.ml')
| -rw-r--r-- | tactics/ind_tables.ml | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/tactics/ind_tables.ml b/tactics/ind_tables.ml index 3cfeed10a0..517ccfaf53 100644 --- a/tactics/ind_tables.ml +++ b/tactics/ind_tables.ml @@ -160,3 +160,5 @@ let define_mutual_scheme kind mode names mind = let check_scheme kind ind = try let _ = find_scheme_on_env_too kind ind in true with Not_found -> false + +let lookup_scheme = DeclareScheme.lookup_scheme |