diff options
| author | Théo Zimmermann | 2018-12-21 17:21:41 +0100 |
|---|---|---|
| committer | Théo Zimmermann | 2018-12-21 17:21:41 +0100 |
| commit | 6c8d47b07b4f0ec59169ac207b204d2bf2116f3a (patch) | |
| tree | 68ae3cefba61118a41a73711a274e1ed7b33f37e | |
| parent | 2b067daecb9529cf77a992c76303d1cc85f11537 (diff) | |
| parent | 9d0087f5e505d5b262bb017a78f6ca9b3eb225ad (diff) | |
Merge PR #9247: Fix typo in gallina specification language doc
| -rw-r--r-- | doc/sphinx/language/gallina-specification-language.rst | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst index 1a33a9a46e..8fa631174f 100644 --- a/doc/sphinx/language/gallina-specification-language.rst +++ b/doc/sphinx/language/gallina-specification-language.rst @@ -230,7 +230,7 @@ There are three sorts :g:`Set`, :g:`Prop` and :g:`Type`. themselves are typing the proofs. We denote propositions by :production:`form`. This constitutes a semantic subclass of the syntactic class :token:`term`. -- :g:`Set` is is the universe of *program types* or *specifications*. The +- :g:`Set` is the universe of *program types* or *specifications*. The specifications themselves are typing the programs. We denote specifications by :production:`specif`. This constitutes a semantic subclass of the syntactic class :token:`term`. |