diff options
Diffstat (limited to 'theories/Program')
| -rw-r--r-- | theories/Program/Basics.v | 8 | ||||
| -rw-r--r-- | theories/Program/Combinators.v | 7 | ||||
| -rw-r--r-- | theories/Program/Equality.v | 2 | ||||
| -rw-r--r-- | theories/Program/Syntax.v | 6 |
4 files changed, 13 insertions, 10 deletions
diff --git a/theories/Program/Basics.v b/theories/Program/Basics.v index c547568816..0a4b15d29d 100644 --- a/theories/Program/Basics.v +++ b/theories/Program/Basics.v @@ -1,3 +1,4 @@ +(* -*- coding: utf-8 -*- *) (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) @@ -9,11 +10,12 @@ (** Standard functions and combinators. - Proofs about them require functional extensionality and can be found in [Combinators]. + Proofs about them require functional extensionality and can be found + in [Combinators]. Author: Matthieu Sozeau - Institution: LRI, CNRS UMR 8623 - Université Paris Sud - 91405 Orsay, France *) + Institution: LRI, CNRS UMR 8623 - University Paris Sud +*) (** The polymorphic identity function is defined in [Datatypes]. *) diff --git a/theories/Program/Combinators.v b/theories/Program/Combinators.v index e12f57668c..31661b9d37 100644 --- a/theories/Program/Combinators.v +++ b/theories/Program/Combinators.v @@ -1,3 +1,4 @@ +(* -*- coding: utf-8 -*- *) (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) @@ -7,11 +8,11 @@ (************************************************************************) (* $Id$ *) -(** Proofs about standard combinators, exports functional extensionality. +(** * Proofs about standard combinators, exports functional extensionality. Author: Matthieu Sozeau - Institution: LRI, CNRS UMR 8623 - UniversitÃcopyright Paris Sud - 91405 Orsay, France *) + Institution: LRI, CNRS UMR 8623 - University Paris Sud +*) Require Import Coq.Program.Basics. Require Export FunctionalExtensionality. diff --git a/theories/Program/Equality.v b/theories/Program/Equality.v index 381a0bae4c..ca65f3bbec 100644 --- a/theories/Program/Equality.v +++ b/theories/Program/Equality.v @@ -1,4 +1,4 @@ -(* -*- coq-prog-name: "~/research/coq/trunk/bin/coqtop.byte"; coq-prog-args: ("-emacs-U"); compile-command: "make -C ../.. TIME='time'" -*- *) +(* -*- coding: utf-8 -*- *) (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) 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. |