diff options
| author | Hugo Herbelin | 2016-09-28 15:29:58 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2016-09-28 16:14:11 +0200 |
| commit | dfadb394640b3d09eb6134b73d0f3e931bd70af1 (patch) | |
| tree | b7f0bba04890b0c905f06829d97d98642168b38f /interp/notation_ops.mli | |
| parent | 8e0f29cb69f06b64d74b18b09fb6a717034f1140 (diff) | |
Warning about similar notations now up to alpha-conversion.
This allows to define on purpose the very same notation in different
files, as currently the notations for *, +, - in Nat.v and Peano.v
(with the first one using variables n and m and the second one using
the default variables used by Infix, namely x and y).
This makes also the "notation-overridden" warning less enigmatic
facing two notations which are the same up to the choice of names.
Diffstat (limited to 'interp/notation_ops.mli')
| -rw-r--r-- | interp/notation_ops.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/interp/notation_ops.mli b/interp/notation_ops.mli index 854e222e30..4ebd3ddd80 100644 --- a/interp/notation_ops.mli +++ b/interp/notation_ops.mli @@ -12,7 +12,7 @@ open Glob_term (** {5 Utilities about [notation_constr]} *) -val eq_notation_constr : notation_constr -> notation_constr -> bool +val eq_notation_constr : Id.t list * Id.t list -> notation_constr -> notation_constr -> bool (** Substitution of kernel names in interpretation data *) |