1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
|
This package was debianized by Fernando Sanchez <fer@debian.org> on
Fri, 3 Dec 1999 22:06:04 +0100.
It was downloaded from ftp://ftp.inria.fr/INRIA/coq
The "Coq proof assistant" was developed conjointly by
INRIA (since 1985),
Laboratoire de l'Informatique du Parallelisme LIP
associated to CNRS and ENS Lyon (sept.89-sept.97),
Laboratoire de Recherche en Informatique
associated to CNRS and Paris 11 (since sept. 97).
The following people have contributed to the core of the system
during the indicated time :
Bruno Barras, (INRIA, 1995-1999)
Cristina Cornes, (INRIA, 1993-1996)
David Delahaye, (INRIA, 1997-1999)
Daniel de Rauglaudre, (INRIA, 1996-1998)
Jean-Christophe Filli�tre, (ENS Lyon, 1994-1997) (Paris 11,1997-1999)
Eduardo Gim�nez, (ENS Lyon, 1993-1996, INRIA, 1997-1998)
Hugo Herbelin, (INRIA, 1996-1999)
G�rard Huet, (INRIA, 1985-1997)
C�sar Mu�oz, (INRIA, 1994-1995)
Chetan Murthy, (INRIA, 1992-1994)
Catherine Parent-Vigouroux, (ENS Lyon 1992-1995)
Patrick Loiseleur, (Paris 11, 1997-1999)
Christine Paulin-Mohring, (INRIA, 1985-1989) (ENS Lyon, 1989-1997)
(Paris 11, 1997-1999)
Amokrane Sa�bi, (INRIA, 1993-1998)
The following directories contain independent contributions:
tactics/contrib/eqdecide
developed by Eduardo Gimenez (INRIA, 1997-1998)
tactics/contrib/extraction
developed by Benjamin Werner (INRIA, 1989)
and Jean-Christophe Filliatre (ENS Lyon, 1994-1997)
tactics/contrib/linear
developed by Jean-Christophe Filliatre (ENS Lyon, 1994-1997)
tactics/contrib/natural
developed by Yann Coscoy (INRIA, 1996)
tactics/contrib/omega
developed by Pierre Cregut (CNET-France Telecom, 1996)
tactics/contrib/pcoq
developed by Yves Bertot (INRIA, 1996-1999)
tactics/contrib/polynom
developed by Samuel Boutin (INRIA, 1996)
and Patrick Loiseleur (LRI, 1997-1999)
tactics/programs
developed by Jean-Christophe Filliatre (LRI, 1997-1999)
theories/REALS
developed by Micaela Mayero (INRIA, 1997-1999)
***************************************************************************
INRIA refers to :
Institute National de la Recherche en Informatique et Automatique
CNRS refers to :
Centre National de la Recherche Scientifique
Paris 11 refers to :
Universite Paris Sud
ENS Lyon refers to :
Ecole Normale Superieure de Lyon
****************************************************************************
Copyright:
All files of the "Coq proof assistant" in directories or sub-directories of
src, tactics, theories, tools
are distributed under the terms of the GNU Lesser General Public License
Version 2.1.
See /usr/share/common-licenses/LGPL-2.1
|
