Return an option in lookup_scheme.

1 files changed, 2 insertions, 4 deletions

diff --git a/tactics/ind_tables.mli b/tactics/ind_tables.mli
index 51f7ef9fd3..9259a4a540 100644
--- a/tactics/ind_tables.mli
+++ b/tactics/ind_tables.mli
@@ -61,10 +61,8 @@ val define_mutual_scheme : mutual scheme_kind -> internal_flag (** internal *) -
 (** Main function to retrieve a scheme in the cache or to generate it *)
 val find_scheme : ?mode:internal_flag -> 'a scheme_kind -> inductive -> Constant.t * Evd.side_effects
 
-val check_scheme : 'a scheme_kind -> inductive -> bool
-
-(** Like [find_scheme] but fails when the scheme is not already in the cache *)
-val lookup_scheme : 'a scheme_kind -> inductive -> Constant.t
+(** Like [find_scheme] but does not generate a constant on the fly *)
+val lookup_scheme : 'a scheme_kind -> inductive -> Constant.t option
 
 val pr_scheme_kind : 'a scheme_kind -> Pp.t