diff options
Diffstat (limited to 'interp/impargs.mli')
| -rw-r--r-- | interp/impargs.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/interp/impargs.mli b/interp/impargs.mli index 8fa69e818a..ef3c2496f4 100644 --- a/interp/impargs.mli +++ b/interp/impargs.mli @@ -68,7 +68,7 @@ type maximal_insertion = bool (** true = maximal contextual insertion *) type force_inference = bool (** true = always infer, never turn into evar/subgoal *) -type implicit_status = (Id.t * implicit_explanation * +type implicit_status = (Constrexpr.explicitation * implicit_explanation * (maximal_insertion * force_inference)) option (** [None] = Not implicit *) |