diff options
Diffstat (limited to 'interp/topconstr.mli')
| -rw-r--r-- | interp/topconstr.mli | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/interp/topconstr.mli b/interp/topconstr.mli index b2d74beed..0064d238d 100644 --- a/interp/topconstr.mli +++ b/interp/topconstr.mli @@ -104,6 +104,8 @@ type binder_kind = (* Inner binding, outer bindings, typeclass-specific flag for implicit generalization of superclasses *) +type abstraction_kind = AbsLambda | AbsPi + type proj_flag = int option (* [Some n] = proj of the n-th visible argument *) type prim_token = Numeral of Bigint.bigint | String of string @@ -144,6 +146,7 @@ type constr_expr = | CSort of loc * rawsort | CCast of loc * constr_expr * constr_expr cast_type | CNotation of loc * notation * constr_expr notation_substitution + | CGeneralization of loc * binding_kind * abstraction_kind option * constr_expr | CPrim of loc * prim_token | CDelimiters of loc * string * constr_expr | CDynamic of loc * Dyn.t |