diff options
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. |