diff options
| author | Pierre Courtieu | 2008-07-21 15:14:58 +0000 |
|---|---|---|
| committer | Pierre Courtieu | 2008-07-21 15:14:58 +0000 |
| commit | a4fe36f5e0c3ffc64797bed551176d6d30a04834 (patch) | |
| tree | ef580b8c356619008d0db0bf0f548b2b6181165f /coq/example-utf8.v | |
| parent | 5b11bdadb77636e56dbfd632c85d443a8e8fe59d (diff) | |
todo added fo coq.
Diffstat (limited to 'coq/example-utf8.v')
| -rw-r--r-- | coq/example-utf8.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/coq/example-utf8.v b/coq/example-utf8.v index 555c7546..4cba17c8 100644 --- a/coq/example-utf8.v +++ b/coq/example-utf8.v @@ -8,7 +8,7 @@ Load "utf8". (* Printing of unicode notation, in *goals* *) -Lemma test : forall A:Prop, A -> A. +Lemma test : ∀ A:Prop, A -> A. auto. Qed. |