diff options
| author | Cyril Anaclet | 2020-04-29 18:10:40 +0200 |
|---|---|---|
| committer | Cyril Anaclet | 2020-04-30 17:09:42 +0200 |
| commit | 0ae25c5ae3f401ad9cabe16b1636ff2e11da874c (patch) | |
| tree | d14d6e162c38b57a0a02e5291e0c34cebd08a136 /ci/test1.v | |
| parent | a2ef60931a194ee441ed0edd5bac68eed3179c50 (diff) | |
[WIP] add 2 tests
Diffstat (limited to 'ci/test1.v')
| -rw-r--r-- | ci/test1.v | 4 |
1 files changed, 2 insertions, 2 deletions
@@ -7,6 +7,6 @@ Eval compute in 10 * trois * trois. Lemma easy_proof : forall A : Prop, A -> A. Proof using . intros A. - intros proof_of_A. + intros proof_of_A. (*test-insert*) exact proof_of_A. -Qed. +Qed. (*test-lemma*) |