diff options
Diffstat (limited to 'intf/evar_kinds.mli')
| -rw-r--r-- | intf/evar_kinds.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/intf/evar_kinds.mli b/intf/evar_kinds.mli index 90ada0e3df..596f6b889a 100644 --- a/intf/evar_kinds.mli +++ b/intf/evar_kinds.mli @@ -17,7 +17,7 @@ open Globnames type obligation_definition_status = Define of bool | Expand type t = - | ImplicitArg of global_reference * (int * identifier option) + | ImplicitArg of global_reference * (int * Id.t option) * bool (** Force inference *) | BinderType of name | QuestionMark of obligation_definition_status @@ -26,4 +26,4 @@ type t = | TomatchTypeParameter of inductive * int | GoalEvar | ImpossibleCase - | MatchingVar of bool * identifier + | MatchingVar of bool * Id.t |