diff options
Diffstat (limited to 'toplevel/ind_tables.mli')
| -rw-r--r-- | toplevel/ind_tables.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/toplevel/ind_tables.mli b/toplevel/ind_tables.mli index 7032eb46e..35ceef86a 100644 --- a/toplevel/ind_tables.mli +++ b/toplevel/ind_tables.mli @@ -41,10 +41,10 @@ val declare_scheme : 'a scheme_kind -> (inductive * constant) array -> unit val define_individual_scheme : individual scheme_kind -> Declare.internal_flag (** internal *) -> - identifier option -> inductive -> constant + Id.t option -> inductive -> constant val define_mutual_scheme : mutual scheme_kind -> Declare.internal_flag (** internal *) -> - (int * identifier) list -> mutual_inductive -> constant array + (int * Id.t) list -> mutual_inductive -> constant array (** Main function to retrieve a scheme in the cache or to generate it *) val find_scheme : 'a scheme_kind -> inductive -> constant |