diff options
| -rwxr-xr-x | theories/Init/Datatypes.v | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v index d216ac2e75..7f86f0cb99 100755 --- a/theories/Init/Datatypes.v +++ b/theories/Init/Datatypes.v @@ -51,6 +51,7 @@ Hints Resolve refl_identity : core v62. Inductive option [A:Set] : Set := Some : A -> (option A) | None : (option A). Implicits None [1]. +V7only [Implicits None [].]. (** [sum A B], equivalently [A + B], is the disjoint sum of [A] and [B] *) (* Syntax defined in Specif.v *) |