aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/constr.ml
diff options
context:
space:
mode:
authorGravatar Pierre Letouzey <pierre.letouzey@inria.fr>2014-12-09 12:48:32 +0100
committerGravatar Pierre Letouzey <pierre.letouzey@inria.fr>2014-12-09 14:27:21 +0100
commitaf84e080ff674a3d5cf2cf88874ddb6ebaf38ecf (patch)
treeb8325cd8ce34dd2dcfba2792a0123cf8c46ab703 /kernel/constr.ml
parent9c24cecec3a7381cd924c56ca50c77a49750e2e5 (diff)
Switch the few remaining iso-latin-1 files to utf8
Diffstat (limited to 'kernel/constr.ml')
-rw-r--r--kernel/constr.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/kernel/constr.ml b/kernel/constr.ml
index f688cca45..0fd4c9d57 100644
--- a/kernel/constr.ml
+++ b/kernel/constr.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* File initially created by Gérard Huet and Thierry Coquand in 1984 *)
+(* File initially created by Gérard Huet and Thierry Coquand in 1984 *)
(* Extension to inductive constructions by Christine Paulin for Coq V5.6 *)
(* Extension to mutual inductive constructions by Christine Paulin for
Coq V5.10.2 *)
@@ -15,7 +15,7 @@
(* Optimization of lifting functions by Bruno Barras, Mar 1997 *)
(* Hash-consing by Bruno Barras in Feb 1998 *)
(* Restructuration of Coq of the type-checking kernel by Jean-Christophe
- Filliâtre, 1999 *)
+ Filliâtre, 1999 *)
(* Abstraction of the syntax of terms and iterators by Hugo Herbelin, 2000 *)
(* Cleaning and lightening of the kernel by Bruno Barras, Nov 2001 *)