diff options
Diffstat (limited to 'intf/constrexpr.mli')
| -rw-r--r-- | intf/constrexpr.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/intf/constrexpr.mli b/intf/constrexpr.mli index 64bbd1e83..af6aea164 100644 --- a/intf/constrexpr.mli +++ b/intf/constrexpr.mli @@ -62,13 +62,13 @@ and cases_pattern_notation_substitution = cases_pattern_expr list list (** for recursive notations *) type constr_expr = - | CRef of reference + | CRef of reference * Univ.universe_instance option | CFix of Loc.t * Id.t located * fix_expr list | CCoFix of Loc.t * Id.t located * cofix_expr list | CProdN of Loc.t * binder_expr list * constr_expr | CLambdaN of Loc.t * binder_expr list * constr_expr | CLetIn of Loc.t * Name.t located * constr_expr * constr_expr - | CAppExpl of Loc.t * (proj_flag * reference) * constr_expr list + | CAppExpl of Loc.t * (proj_flag * reference * Univ.universe_instance option) * constr_expr list | CApp of Loc.t * (proj_flag * constr_expr) * (constr_expr * explicitation located option) list | CRecord of Loc.t * constr_expr option * (reference * constr_expr) list |