summaryrefslogtreecommitdiff
path: root/theories/Program
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2010-07-24 20:01:08 +0200
committerGravatar Stephane Glondu <steph@glondu.net>2010-07-24 20:01:08 +0200
commitb9f47391f7f259c24119d1de0a87839e2cc5e80c (patch)
tree26dd3d5de63f420384fd84196d3a144af01f6084 /theories/Program
parent5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 (diff)
Imported Upstream snapshot 8.3~beta0+13323
Diffstat (limited to 'theories/Program')
-rw-r--r--theories/Program/Basics.v2
-rw-r--r--theories/Program/Combinators.v2
-rw-r--r--theories/Program/Equality.v2
-rw-r--r--theories/Program/Program.v2
-rw-r--r--theories/Program/Subset.v2
-rw-r--r--theories/Program/Syntax.v2
-rw-r--r--theories/Program/Tactics.v2
-rw-r--r--theories/Program/Utils.v2
-rw-r--r--theories/Program/Wf.v2
9 files changed, 9 insertions, 9 deletions
diff --git a/theories/Program/Basics.v b/theories/Program/Basics.v
index 0a4b15d2..f4017024 100644
--- a/theories/Program/Basics.v
+++ b/theories/Program/Basics.v
@@ -1,7 +1,7 @@
(* -*- coding: utf-8 -*- *)
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/theories/Program/Combinators.v b/theories/Program/Combinators.v
index 31661b9d..39fb4093 100644
--- a/theories/Program/Combinators.v
+++ b/theories/Program/Combinators.v
@@ -1,7 +1,7 @@
(* -*- coding: utf-8 -*- *)
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/theories/Program/Equality.v b/theories/Program/Equality.v
index 79c9bec5..1e139497 100644
--- a/theories/Program/Equality.v
+++ b/theories/Program/Equality.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/theories/Program/Program.v b/theories/Program/Program.v
index cdfc7858..71be3478 100644
--- a/theories/Program/Program.v
+++ b/theories/Program/Program.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/theories/Program/Subset.v b/theories/Program/Subset.v
index 89f477d8..ce5f1068 100644
--- a/theories/Program/Subset.v
+++ b/theories/Program/Subset.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/theories/Program/Syntax.v b/theories/Program/Syntax.v
index 2064977f..05bf2ea6 100644
--- a/theories/Program/Syntax.v
+++ b/theories/Program/Syntax.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/theories/Program/Tactics.v b/theories/Program/Tactics.v
index e692876d..91a8edff 100644
--- a/theories/Program/Tactics.v
+++ b/theories/Program/Tactics.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/theories/Program/Utils.v b/theories/Program/Utils.v
index fbf0b03c..f2aad800 100644
--- a/theories/Program/Utils.v
+++ b/theories/Program/Utils.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/theories/Program/Wf.v b/theories/Program/Wf.v
index 98b1c619..d16e900f 100644
--- a/theories/Program/Wf.v
+++ b/theories/Program/Wf.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)