diff options
| author | Cyril Cohen | 2018-02-21 15:10:05 +0100 |
|---|---|---|
| committer | GitHub | 2018-02-21 15:10:05 +0100 |
| commit | 13f26ccc09f87b222f9601892f085276a6ddb8c0 (patch) | |
| tree | d5b8ee38a7ba049d3d7b2da5c9edfe0f51ba1ec8 /mathcomp/ssrtest | |
| parent | d6bc72cd477ed6fe8b95782b26a2e0fc92711395 (diff) | |
| parent | 3b2fd56a5645b3bd436085e514519c9f61200ae5 (diff) | |
Merge pull request #177 from gares/fix/missing-ssrtest-in-Make
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. |