aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/recordops.mli
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping/recordops.mli')
-rw-r--r--pretyping/recordops.mli4
1 files changed, 2 insertions, 2 deletions
diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli
index 538e6d540..6afba15bf 100644
--- a/pretyping/recordops.mli
+++ b/pretyping/recordops.mli
@@ -22,11 +22,11 @@ open Library
type struc_typ = {
s_CONST : constructor;
s_EXPECTEDPARAM : int;
- s_PROJKIND : (name * bool) list;
+ s_PROJKIND : (Name.t * bool) list;
s_PROJ : constant option list }
type struc_tuple =
- inductive * constructor * (name * bool) list * constant option list
+ inductive * constructor * (Name.t * bool) list * constant option list
val declare_structure : struc_tuple -> unit