diff options
Diffstat (limited to 'tactics/ind_tables.mli')
| -rw-r--r-- | tactics/ind_tables.mli | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/tactics/ind_tables.mli b/tactics/ind_tables.mli index dad2036c64..736de2af37 100644 --- a/tactics/ind_tables.mli +++ b/tactics/ind_tables.mli @@ -59,3 +59,11 @@ val check_scheme : 'a scheme_kind -> inductive -> bool val lookup_scheme : 'a scheme_kind -> inductive -> Constant.t val pr_scheme_kind : 'a scheme_kind -> Pp.t + +val declare_definition_scheme : + (internal : bool + -> univs:Entries.universes_entry + -> role:Evd.side_effect_role + -> name:Id.t + -> Constr.t + -> Constant.t * Evd.side_effects) ref |