diff options
Diffstat (limited to 'pretyping/classops.mli')
| -rw-r--r-- | pretyping/classops.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/classops.mli b/pretyping/classops.mli index a4bf0ee8fc..fe7fb437da 100644 --- a/pretyping/classops.mli +++ b/pretyping/classops.mli @@ -16,7 +16,7 @@ type cl_typ = | CL_FUN | CL_Var of identifier | CL_SP of section_path - | CL_IND of section_path * int + | CL_IND of inductive_path type cl_info_typ = { cL_STR : string; |