diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/rawterm.ml | 4 | ||||
| -rw-r--r-- | pretyping/rawterm.mli | 4 |
2 files changed, 2 insertions, 6 deletions
diff --git a/pretyping/rawterm.ml b/pretyping/rawterm.ml index c3f7d8822c..ec43265658 100644 --- a/pretyping/rawterm.ml +++ b/pretyping/rawterm.ml @@ -30,13 +30,11 @@ type reference = | REVar of int * identifier list | RMeta of int -type cases_style = PrintLet | PrintIf | PrintCases - type rawconstr = | RRef of loc * reference | RApp of loc * rawconstr * rawconstr list | RBinder of loc * binder_kind * name * rawconstr * rawconstr - | RCases of loc * cases_style * rawconstr option * rawconstr list * + | RCases of loc * Term.case_style * rawconstr option * rawconstr list * (identifier list * pattern list * rawconstr) list | ROldCase of loc * bool * rawconstr option * rawconstr * rawconstr array diff --git a/pretyping/rawterm.mli b/pretyping/rawterm.mli index 8c93eecd9f..c31691046d 100644 --- a/pretyping/rawterm.mli +++ b/pretyping/rawterm.mli @@ -30,13 +30,11 @@ type reference = | REVar of int * identifier list | RMeta of int -type cases_style = PrintLet | PrintIf | PrintCases - type rawconstr = | RRef of loc * reference | RApp of loc * rawconstr * rawconstr list | RBinder of loc * binder_kind * name * rawconstr * rawconstr - | RCases of loc * cases_style * rawconstr option * rawconstr list * + | RCases of loc * Term.case_style * rawconstr option * rawconstr list * (identifier list * pattern list * rawconstr) list | ROldCase of loc * bool * rawconstr option * rawconstr * rawconstr array |