summaryrefslogtreecommitdiff
path: root/test-suite/success/Require.v
blob: f851d8c7d9d87a2e8f0cf7b138056b571f7c54b0 (plain)
1
2
3
Require Import Coq.Arith.Plus.
Require Coq.Arith.Minus.
Locate Library Coq.Arith.Minus.