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 /tactics | |
| parent | 504b1b71ed56431c978b9bbf46c4d67f155fddf2 (diff) | |
Make explicit that users should not observe return values of scheme functions.
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/ind_tables.ml | 6 | ||||
| -rw-r--r-- | tactics/ind_tables.mli | 4 |
2 files changed, 8 insertions, 2 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 |