From 300293c119981054c95182a90c829058530a6b6f Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Sun, 25 Dec 2011 13:19:42 +0100
Subject: Imported Upstream version 8.3.pl3

---
 plugins/cc/ccalgo.ml        | 4 ++--
 plugins/cc/ccalgo.mli       | 4 ++--
 plugins/cc/ccproof.ml       | 4 ++--
 plugins/cc/ccproof.mli      | 4 ++--
 plugins/cc/cctac.ml         | 4 ++--
 plugins/cc/cctac.mli        | 4 ++--
 plugins/cc/g_congruence.ml4 | 4 ++--
 7 files changed, 14 insertions(+), 14 deletions(-)

(limited to 'plugins/cc')

diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml
index 82b4143e..3c40cfb9 100644
--- a/plugins/cc/ccalgo.ml
+++ b/plugins/cc/ccalgo.ml
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: ccalgo.ml 13409 2010-09-13 07:53:13Z soubiran $ *)
+(* $Id: ccalgo.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
 
 (* This file implements the basic congruence-closure algorithm by *)
 (* Downey,Sethi and Tarjan. *)
diff --git a/plugins/cc/ccalgo.mli b/plugins/cc/ccalgo.mli
index 2825be1a..8786c907 100644
--- a/plugins/cc/ccalgo.mli
+++ b/plugins/cc/ccalgo.mli
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: ccalgo.mli 13323 2010-07-24 15:57:30Z herbelin $ *)
+(* $Id: ccalgo.mli 14641 2011-11-06 11:59:10Z herbelin $ *)
 
 open Util
 open Term
diff --git a/plugins/cc/ccproof.ml b/plugins/cc/ccproof.ml
index 5ee17b6e..6981c5a0 100644
--- a/plugins/cc/ccproof.ml
+++ b/plugins/cc/ccproof.ml
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: ccproof.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
+(* $Id: ccproof.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
 
 (* This file uses the (non-compressed) union-find structure to generate *)
 (* proof-trees that will be transformed into proof-terms in cctac.ml4   *)
diff --git a/plugins/cc/ccproof.mli b/plugins/cc/ccproof.mli
index 4c75f9b0..a58637f9 100644
--- a/plugins/cc/ccproof.mli
+++ b/plugins/cc/ccproof.mli
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: ccproof.mli 13323 2010-07-24 15:57:30Z herbelin $ *)
+(* $Id: ccproof.mli 14641 2011-11-06 11:59:10Z herbelin $ *)
 
 open Ccalgo
 open Names
diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index ca1a9085..5b477b4d 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -8,7 +8,7 @@
 
 (*i camlp4deps: "parsing/grammar.cma" i*)
 
-(* $Id: cctac.ml 13409 2010-09-13 07:53:13Z soubiran $ *)
+(* $Id: cctac.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
 
 (* This file is the interface between the c-c algorithm and Coq *)
 
diff --git a/plugins/cc/cctac.mli b/plugins/cc/cctac.mli
index 1c07cabf..b3d5c16b 100644
--- a/plugins/cc/cctac.mli
+++ b/plugins/cc/cctac.mli
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: cctac.mli 13323 2010-07-24 15:57:30Z herbelin $ *)
+(* $Id: cctac.mli 14641 2011-11-06 11:59:10Z herbelin $ *)
 
 open Term
 open Proof_type
diff --git a/plugins/cc/g_congruence.ml4 b/plugins/cc/g_congruence.ml4
index bed77a7b..eb58c5eb 100644
--- a/plugins/cc/g_congruence.ml4
+++ b/plugins/cc/g_congruence.ml4
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -8,7 +8,7 @@
 
 (*i camlp4deps: "parsing/grammar.cma" i*)
 
-(* $Id: g_congruence.ml4 13323 2010-07-24 15:57:30Z herbelin $ *)
+(* $Id: g_congruence.ml4 14641 2011-11-06 11:59:10Z herbelin $ *)
 
 open Cctac
 open Tactics
-- 
cgit v1.2.3