diff options
Diffstat (limited to 'vernac/record.mli')
| -rw-r--r-- | vernac/record.mli | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/vernac/record.mli b/vernac/record.mli index 7a40af048c..feb257da3c 100644 --- a/vernac/record.mli +++ b/vernac/record.mli @@ -11,6 +11,7 @@ open Names open Vernacexpr open Constrexpr +open Structures module Ast : sig type t = @@ -51,8 +52,8 @@ module Internal : sig -> projection_flags list -> Impargs.manual_implicits list -> Constr.rel_context - -> Recordops.proj_kind list * Names.Constant.t option list + -> Structure.projection list - val declare_structure_entry : Recordops.struc_typ -> unit + val declare_structure_entry : Structure.t -> unit end |