diff options
Diffstat (limited to 'pretyping/rawterm.mli')
| -rw-r--r-- | pretyping/rawterm.mli | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/pretyping/rawterm.mli b/pretyping/rawterm.mli index 5115e2d59..3628e2a50 100644 --- a/pretyping/rawterm.mli +++ b/pretyping/rawterm.mli @@ -66,7 +66,6 @@ type rawconstr = | RLambda of loc * name * binding_kind * rawconstr * rawconstr | RProd of loc * name * binding_kind * rawconstr * rawconstr | RLetIn of loc * name * rawconstr * rawconstr - | RRecord of loc * rawconstr option * ((loc * identifier) * rawconstr) list | RCases of loc * case_style * rawconstr option * tomatch_tuples * cases_clauses | RLetTuple of loc * name list * (name * rawconstr option) * rawconstr * rawconstr |