diff options
| author | Pierre-Marie Pédrot | 2019-12-10 09:05:05 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-12-10 10:53:54 +0100 |
| commit | 50221b84f6af681f69e8f9847a851329a4662509 (patch) | |
| tree | 735a0ac6f2f1d1f1e62b8c1116e7830fde5c1758 /vernac/indschemes.ml | |
| parent | 504b1b71ed56431c978b9bbf46c4d67f155fddf2 (diff) | |
Make explicit that users should not observe return values of scheme functions.
Diffstat (limited to 'vernac/indschemes.ml')
| -rw-r--r-- | vernac/indschemes.ml | 18 |
1 files changed, 9 insertions, 9 deletions
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 |