diff options
Diffstat (limited to 'theories/Init/Datatypes.v')
| -rwxr-xr-x | theories/Init/Datatypes.v | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v index c0c999c4c..cb2c27284 100755 --- a/theories/Init/Datatypes.v +++ b/theories/Init/Datatypes.v @@ -74,8 +74,10 @@ Section projections. Definition snd := [p:(prod A B)]Cases p of (pair x y) => y end. End projections. +V7only [ Notation Fst := (fst ? ?). Notation Snd := (snd ? ?). +]. Hints Resolve pair inl inr : core v62. |