diff options
| author | Hugo Herbelin | 2017-08-09 13:58:59 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2018-02-20 10:03:04 +0100 |
| commit | 51976c9f2157953f794ed1efcd68403a8545d346 (patch) | |
| tree | 612cc59179d2d16d5bb552f31f0abda92e50dd23 /intf/notation_term.ml | |
| parent | 6901f720c6115c8eec1343846641a5c8453c3268 (diff) | |
A bit of miscellaneous code documentation around notations.
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 d1cbb6a33d..028d14ccfd 100644 --- a/intf/notation_term.ml +++ b/intf/notation_term.ml @@ -63,7 +63,7 @@ type subscopes = tmp_scope_name option * scope_name list type notation_var_instance_type = | NtnTypeConstr | NtnTypeOnlyBinder | NtnTypeConstrList | NtnTypeBinderList -(** Type of variables when interpreting a constr_expr as an notation_constr: +(** Type of variables when interpreting a constr_expr as a notation_constr: in a recursive pattern x..y, both x and y carry the individual type of each element of the list x..y *) type notation_var_internalization_type = |