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