aboutsummaryrefslogtreecommitdiff
path: root/theories/Program/Syntax.v
diff options
context:
space:
mode:
Diffstat (limited to 'theories/Program/Syntax.v')
-rw-r--r--theories/Program/Syntax.v6
1 files changed, 3 insertions, 3 deletions
diff --git a/theories/Program/Syntax.v b/theories/Program/Syntax.v
index 9828d4b693..aff2da946e 100644
--- a/theories/Program/Syntax.v
+++ b/theories/Program/Syntax.v
@@ -10,10 +10,10 @@
(** Custom notations and implicits for Coq prelude definitions.
Author: Matthieu Sozeau
- Institution: LRI, CNRS UMR 8623 - UniversitÃcopyright Paris Sud
- 91405 Orsay, France *)
+ Institution: LRI, CNRS UMR 8623 - University Paris Sud
+*)
-(** Notations for the unit type and value à la Haskell. *)
+(** Haskell-style notations for the unit type and value. *)
Notation " () " := Datatypes.unit : type_scope.
Notation " () " := tt.