diff options
Diffstat (limited to 'intf/notation_term.ml')
| -rw-r--r-- | intf/notation_term.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/intf/notation_term.ml b/intf/notation_term.ml index c342da3dc..7823d3feb 100644 --- a/intf/notation_term.ml +++ b/intf/notation_term.ml @@ -31,7 +31,7 @@ type notation_constr = | NProd of Name.t * notation_constr * notation_constr | NBinderList of Id.t * Id.t * notation_constr * notation_constr | NLetIn of Name.t * notation_constr * notation_constr option * notation_constr - | NCases of case_style * notation_constr option * + | NCases of Constr.case_style * notation_constr option * (notation_constr * (Name.t * (inductive * Name.t list) option)) list * (cases_pattern list * notation_constr) list | NLetTuple of Name.t list * (Name.t * notation_constr option) * |