diff options
| author | Pierre-Marie Pédrot | 2020-04-28 16:21:33 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-04-28 16:31:43 +0200 |
| commit | 3ff3c18031317dcd08bf081e55212617b8820647 (patch) | |
| tree | 420126181a1158afda19a649e388e306f41d723c /tactics/ind_tables.ml | |
| parent | 2c04f5df480492169e533c376cc50caff863ba5a (diff) | |
Return an option in lookup_scheme.
Diffstat (limited to 'tactics/ind_tables.ml')
| -rw-r--r-- | tactics/ind_tables.ml | 9 |
1 files changed, 4 insertions, 5 deletions
diff --git a/tactics/ind_tables.ml b/tactics/ind_tables.ml index 511cbb8b18..ae27cf1019 100644 --- a/tactics/ind_tables.ml +++ b/tactics/ind_tables.ml @@ -93,9 +93,10 @@ let compute_name internal id = let declare_definition_scheme = ref (fun ~internal ~univs ~role ~name c -> CErrors.anomaly (Pp.str "scheme declaration not registered")) -let check_scheme kind ind = - try let _ = DeclareScheme.lookup_scheme kind ind in true - with Not_found -> false +let lookup_scheme kind ind = + try Some (DeclareScheme.lookup_scheme kind ind) with Not_found -> None + +let check_scheme kind ind = Option.has_some (lookup_scheme kind ind) let define internal role id c poly univs = let id = compute_name internal id in @@ -187,5 +188,3 @@ let define_individual_scheme kind mode names ind = let define_mutual_scheme kind mode names mind = ignore (define_mutual_scheme kind mode names mind) - -let lookup_scheme = DeclareScheme.lookup_scheme |