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 | |
| 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')
| -rw-r--r-- | mathcomp/Make | 3 | ||||
| -rw-r--r-- | mathcomp/ssrtest/explain_match.v | 3 |
2 files changed, 5 insertions, 1 deletions
diff --git a/mathcomp/Make b/mathcomp/Make index e259330..d3c7642 100644 --- a/mathcomp/Make +++ b/mathcomp/Make @@ -132,15 +132,18 @@ ssreflect/ssrnat.v ssreflect/ssrnotations.v ssreflect/tuple.v ssrtest/absevarprop.v +ssrtest/abstract_var2.v ssrtest/binders_of.v ssrtest/binders.v ssrtest/caseview.v ssrtest/congr.v ssrtest/deferclear.v +ssrtest/derive_inversion.v ssrtest/dependent_type_err.v ssrtest/elim2.v ssrtest/elim_pattern.v ssrtest/elim.v +ssrtest/explain_match.v ssrtest/first_n.v ssrtest/gen_have.v ssrtest/gen_pattern.v 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. |