diff options
| author | Hugo Herbelin | 2020-10-24 14:45:57 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-11-20 19:41:20 +0100 |
| commit | 93654a0ba50f26f90f84e98b33ec13caa92d1799 (patch) | |
| tree | 9ee57efbb938eeadf37e0ea80ba73bd7cb0a1722 /interp/notation_term.ml | |
| parent | 23924afa0e4d7ed9ca58fbf5f69dc57685d593fa (diff) | |
Enforcing when a binding variable has no explicit type in constr_notation.
This avoids relying on fragile invariants.
Diffstat (limited to 'interp/notation_term.ml')
| -rw-r--r-- | interp/notation_term.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/interp/notation_term.ml b/interp/notation_term.ml index 47b9deccce..29db23cc54 100644 --- a/interp/notation_term.ml +++ b/interp/notation_term.ml @@ -27,8 +27,8 @@ type notation_constr = | NHole of Evar_kinds.t * Namegen.intro_pattern_naming_expr * Genarg.glob_generic_argument option | NList of Id.t * Id.t * notation_constr * notation_constr * (* associativity: *) bool (* Part only in [glob_constr] *) - | NLambda of Name.t * notation_constr * notation_constr - | NProd of Name.t * notation_constr * notation_constr + | NLambda of Name.t * notation_constr option * notation_constr + | NProd of Name.t * notation_constr option * notation_constr | NBinderList of Id.t * Id.t * notation_constr * notation_constr * (* associativity: *) bool | NLetIn of Name.t * notation_constr * notation_constr option * notation_constr | NCases of Constr.case_style * notation_constr option * |