diff options
| author | Enrico Tassi | 2018-02-06 13:52:29 +0100 |
|---|---|---|
| committer | Enrico Tassi | 2018-02-06 15:46:26 +0100 |
| commit | 3b2fd56a5645b3bd436085e514519c9f61200ae5 (patch) | |
| tree | 367841c04d6b97dd0776bf15c4ff63805b2dfd72 /mathcomp/ssrtest | |
| parent | 64c6b07ff318b9eee032e929f0cd25b2e2ddaeda (diff) | |
add 3 tests to Make
Diffstat (limited to 'mathcomp/ssrtest')
| -rw-r--r-- | mathcomp/ssrtest/explain_match.v | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/mathcomp/ssrtest/explain_match.v b/mathcomp/ssrtest/explain_match.v index b79453b..2c7bc2f 100644 --- a/mathcomp/ssrtest/explain_match.v +++ b/mathcomp/ssrtest/explain_match.v @@ -1,3 +1,4 @@ +Require Import ssrmatching. Require Import ssreflect ssrbool ssrnat. Definition addnAC := (addnA, addnC). @@ -9,4 +10,4 @@ ssrinstancesofruleL2R addnC. ssrinstancesofruleR2L addnA. ssrinstancesofruleR2L addnAC. Fail ssrinstancesoftpat (_ + _ in RHS). (* Not implemented *) -Admitted.
\ No newline at end of file +Admitted. |