Return an option in lookup_scheme.

7 files changed, 24 insertions, 25 deletions

diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index f002bbc57a..3834b21a14 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -952,10 +952,11 @@ let fold_match env sigma c =
         then case_dep_scheme_kind_from_type
         else case_scheme_kind_from_type)
     in
-    let exists = Ind_tables.check_scheme sk ci.ci_ind in
-      if exists then
-        dep, pred, exists, Ind_tables.lookup_scheme sk ci.ci_ind
-      else raise Not_found
+    match Ind_tables.lookup_scheme sk ci.ci_ind with
+    | Some cst ->
+        dep, pred, true, cst
+    | None ->
+      raise Not_found
   in
   let app =
     let ind, args = Inductiveops.find_mrectype env sigma cty in
diff --git a/tactics/elimschemes.ml b/tactics/elimschemes.ml
index b08f4c8be7..9a517652a7 100644
--- a/tactics/elimschemes.ml
+++ b/tactics/elimschemes.ml
@@ -27,11 +27,11 @@ open Ind_tables
 let optimize_non_type_induction_scheme kind dep sort ind =
   let env = Global.env () in
   let sigma = Evd.from_env env in
-  if check_scheme kind ind then
+  match lookup_scheme kind ind with
+  | Some cte ->
     (* in case the inductive has a type elimination, generates only one
        induction scheme, the other ones share the same code with the
        appropriate type *)
-    let cte = lookup_scheme kind ind in
     let sigma, cte = Evd.fresh_constant_instance env sigma cte in
     let c = mkConstU cte in
     let t = type_of_constant_in (Global.env()) cte in
@@ -48,7 +48,7 @@ let optimize_non_type_induction_scheme kind dep sort ind =
     let sigma, t', c' = weaken_sort_scheme env sigma false sort npars c t in
     let sigma = Evd.minimize_universes sigma in
     (Evarutil.nf_evars_universes sigma c', Evd.evar_universe_context sigma)
-  else
+  | None ->
     let sigma, pind = Evd.fresh_inductive_instance ~rigid:UState.univ_rigid env sigma ind in
     let sigma, c = build_induction_scheme env sigma pind dep sort in
       (c, Evd.evar_universe_context sigma)
diff --git a/tactics/eqschemes.ml b/tactics/eqschemes.ml
index 000896bfea..7c702eab3a 100644
--- a/tactics/eqschemes.ml
+++ b/tactics/eqschemes.ml
@@ -248,8 +248,7 @@ let sym_scheme_kind =
 (**********************************************************************)
 
 let const_of_scheme kind env ind ctx =
-  let () = assert (check_scheme kind ind) in
-  let sym_scheme = lookup_scheme kind ind in
+  let sym_scheme = match lookup_scheme kind ind with Some cst -> cst | None -> assert false in
   let sym, ctx = with_context_set ctx
     (UnivGen.fresh_constant_instance (Global.env()) sym_scheme) in
     mkConstU sym, ctx
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 49645d82a4..8f2336c0e0 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -1347,7 +1347,7 @@ let inject_if_homogenous_dependent_pair ty =
     (* and compare the fst arguments of the dep pair *)
     (* Note: should work even if not an inductive type, but the table only *)
     (* knows inductive types *)
-    if not (Ind_tables.check_scheme (!eq_dec_scheme_kind_name()) ind &&
+    if not (Option.has_some (Ind_tables.lookup_scheme (!eq_dec_scheme_kind_name()) ind) &&
       pf_apply is_conv gl ar1.(2) ar2.(2)) then raise Exit;
     check_required_library ["Coq";"Logic";"Eqdep_dec"];
     let new_eq_args = [|pf_get_type_of gl ar1.(3);ar1.(3);ar2.(3)|] in
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
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
 
diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml
index b5f832d34d..f8a2d15661 100644
--- a/vernac/auto_ind_decl.ml
+++ b/vernac/auto_ind_decl.ml
@@ -251,9 +251,10 @@ let build_beq_scheme mode kn =
             if MutInd.equal kn kn' then mkRel(eqA-nlist-i+nb_ind-1)
             else begin
               try
-                let () = assert (check_scheme (!beq_scheme_kind_aux()) ind') in
-                let c = lookup_scheme (!beq_scheme_kind_aux()) ind' in
-                let eq = mkConst c in
+                let eq = match lookup_scheme (!beq_scheme_kind_aux()) ind' with
+                | Some c -> mkConst c
+                | None -> assert false
+                in
                 let eqa = Array.of_list @@ List.map aux a in
                 let args =
                   Array.append
@@ -586,9 +587,10 @@ let eqI ind l =
   let list_id = list_id l in
   let eA = Array.of_list((List.map (fun (s,_,_,_) -> mkVar s) list_id)@
                            (List.map (fun (_,seq,_,_)-> mkVar seq) list_id ))
-  and e =
-    try let c = lookup_scheme beq_scheme_kind ind in mkConst c
-    with Not_found -> user_err ~hdr:"AutoIndDecl.eqI"
+  and e = match lookup_scheme beq_scheme_kind ind with
+  | Some c -> mkConst c
+  | None ->
+    user_err ~hdr:"AutoIndDecl.eqI"
       (str "The boolean equality on " ++ Printer.pr_inductive (Global.env ()) ind ++ str " is needed.");
   in (if Array.equal Constr.equal eA [||] then e else mkApp(e,eA))