aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/rtauto/refl_tauto.ml
diff options
context:
space:
mode:
authorGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2010-07-24 15:57:30 +0000
committerGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2010-07-24 15:57:30 +0000
commit8d99bfcdc0915c006bffba6d5ffe14c683b9eb65 (patch)
treef66bf6b10fae56354ae82f811c2a8273d5d30e13 /plugins/rtauto/refl_tauto.ml
parent27882e4edd07e306333fdc024330982741416a19 (diff)
Updated all headers for 8.3 and trunk
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13323 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins/rtauto/refl_tauto.ml')
-rw-r--r--plugins/rtauto/refl_tauto.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/rtauto/refl_tauto.ml b/plugins/rtauto/refl_tauto.ml
index 3ae25da65..3e9cc781f 100644
--- a/plugins/rtauto/refl_tauto.ml
+++ b/plugins/rtauto/refl_tauto.ml
@@ -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 *)