aboutsummaryrefslogtreecommitdiffhomepage
path: root/intf/evar_kinds.mli
diff options
context:
space:
mode:
Diffstat (limited to 'intf/evar_kinds.mli')
-rw-r--r--intf/evar_kinds.mli2
1 files changed, 1 insertions, 1 deletions
diff --git a/intf/evar_kinds.mli b/intf/evar_kinds.mli
index 596f6b889..1541d4e46 100644
--- a/intf/evar_kinds.mli
+++ b/intf/evar_kinds.mli
@@ -19,7 +19,7 @@ type obligation_definition_status = Define of bool | Expand
type t =
| ImplicitArg of global_reference * (int * Id.t option)
* bool (** Force inference *)
- | BinderType of name
+ | BinderType of Name.t
| QuestionMark of obligation_definition_status
| CasesType
| InternalHole