Make explicit that users should not observe return values of scheme functions.

3 files changed, 17 insertions, 11 deletions

diff --git a/tactics/ind_tables.ml b/tactics/ind_tables.ml
index 3c0cf1a3c0..3cfeed10a0 100644
--- a/tactics/ind_tables.ml
+++ b/tactics/ind_tables.ml
@@ -151,6 +151,12 @@ let find_scheme ?(mode=InternalTacticRequest) kind (mind,i as ind) =
       let ca, eff = define_mutual_scheme_base kind s f mode [] mind in
       ca.(i), eff
 
+let define_individual_scheme kind mode names ind =
+  ignore (define_individual_scheme kind mode names ind)
+
+let define_mutual_scheme kind mode names mind =
+  ignore (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
diff --git a/tactics/ind_tables.mli b/tactics/ind_tables.mli
index 7e544b09dc..60044bf460 100644
--- a/tactics/ind_tables.mli
+++ b/tactics/ind_tables.mli
@@ -45,10 +45,10 @@ val declare_individual_scheme_object : string -> ?aux:string ->
 
 val define_individual_scheme : individual scheme_kind ->
   internal_flag (** internal *) ->
-  Id.t option -> inductive -> Constant.t * Evd.side_effects
+  Id.t option -> inductive -> unit
 
 val define_mutual_scheme : mutual scheme_kind -> internal_flag (** internal *) ->
-  (int * Id.t) list -> MutInd.t -> Constant.t array * Evd.side_effects
+  (int * Id.t) list -> MutInd.t -> unit
 
 (** 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
diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml
index b2e1a5e796..2f0b1062a7 100644
--- a/vernac/indschemes.ml
+++ b/vernac/indschemes.ml
@@ -210,7 +210,7 @@ let declare_one_case_analysis_scheme ind =
        induction scheme, the other ones share the same code with the
        appropriate type *)
   if Sorts.family_leq InType kelim then
-    ignore (define_individual_scheme dep UserAutomaticRequest None ind)
+    define_individual_scheme dep UserAutomaticRequest None ind
 
 (* Induction/recursion schemes *)
 
@@ -248,7 +248,7 @@ let declare_one_induction_scheme ind =
        else if depelim then kinds_from_type
        else nondep_kinds_from_type)
   in
-  List.iter (fun kind -> ignore (define_individual_scheme kind UserAutomaticRequest None ind))
+  List.iter (fun kind -> define_individual_scheme kind UserAutomaticRequest None ind)
     elims
 
 let declare_induction_schemes kn =
@@ -264,7 +264,7 @@ let declare_induction_schemes kn =
 let declare_eq_decidability_gen internal names kn =
   let mib = Global.lookup_mind kn in
   if mib.mind_finite <> Declarations.CoFinite then
-    ignore (define_mutual_scheme eq_dec_scheme_kind internal names kn)
+    define_mutual_scheme eq_dec_scheme_kind internal names kn
 
 let eq_dec_scheme_msg ind = (* TODO: mutual inductive case *)
   str "Decidable equality on " ++ quote (Printer.pr_inductive (Global.env()) ind)
@@ -280,14 +280,14 @@ let try_declare_eq_decidability kn =
 let declare_eq_decidability = declare_eq_decidability_scheme_with []
 
 let ignore_error f x =
-  try ignore (f x) with e when CErrors.noncritical e -> ()
+  try f x with e when CErrors.noncritical e -> ()
 
 let declare_rewriting_schemes ind =
   if Hipattern.is_inductive_equality ind then begin
-    ignore (define_individual_scheme rew_r2l_scheme_kind UserAutomaticRequest None ind);
-    ignore (define_individual_scheme rew_r2l_dep_scheme_kind UserAutomaticRequest None ind);
-    ignore (define_individual_scheme rew_r2l_forward_dep_scheme_kind
-      UserAutomaticRequest None ind);
+    define_individual_scheme rew_r2l_scheme_kind UserAutomaticRequest None ind;
+    define_individual_scheme rew_r2l_dep_scheme_kind UserAutomaticRequest None ind;
+    define_individual_scheme rew_r2l_forward_dep_scheme_kind
+      UserAutomaticRequest None ind;
     (* These ones expect the equality to be symmetric; the first one also *)
     (* needs eq *)
     ignore_error (define_individual_scheme rew_l2r_scheme_kind UserAutomaticRequest None) ind;
@@ -310,7 +310,7 @@ let declare_congr_scheme ind =
       try Coqlib.check_required_library Coqlib.logic_module_name; true
       with e when CErrors.noncritical e -> false
     then
-      ignore (define_individual_scheme congr_scheme_kind UserAutomaticRequest None ind)
+      define_individual_scheme congr_scheme_kind UserAutomaticRequest None ind
     else
       warn_cannot_build_congruence ()
   end