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/firstorder/formula.ml    | 4 ++--
 plugins/firstorder/formula.mli   | 4 ++--
 plugins/firstorder/g_ground.ml4  | 4 ++--
 plugins/firstorder/ground.ml     | 4 ++--
 plugins/firstorder/ground.mli    | 4 ++--
 plugins/firstorder/instances.ml  | 4 ++--
 plugins/firstorder/instances.mli | 4 ++--
 plugins/firstorder/rules.ml      | 4 ++--
 plugins/firstorder/rules.mli     | 4 ++--
 plugins/firstorder/sequent.ml    | 4 ++--
 plugins/firstorder/sequent.mli   | 4 ++--
 plugins/firstorder/unify.ml      | 4 ++--
 plugins/firstorder/unify.mli     | 4 ++--
 13 files changed, 26 insertions(+), 26 deletions(-)

(limited to 'plugins/firstorder')

diff --git a/plugins/firstorder/formula.ml b/plugins/firstorder/formula.ml
index d039a930..1f3fd595 100644
--- a/plugins/firstorder/formula.ml
+++ b/plugins/firstorder/formula.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: formula.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
+(* $Id: formula.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
 
 open Hipattern
 open Names
diff --git a/plugins/firstorder/formula.mli b/plugins/firstorder/formula.mli
index fbb103c0..a831c087 100644
--- a/plugins/firstorder/formula.mli
+++ b/plugins/firstorder/formula.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: formula.mli 13323 2010-07-24 15:57:30Z herbelin $ *)
+(* $Id: formula.mli 14641 2011-11-06 11:59:10Z herbelin $ *)
 
 open Term
 open Names
diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4
index 19b63407..8e68506c 100644
--- a/plugins/firstorder/g_ground.ml4
+++ b/plugins/firstorder/g_ground.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_ground.ml4 13344 2010-07-28 15:04:36Z msozeau $ *)
+(* $Id: g_ground.ml4 14641 2011-11-06 11:59:10Z herbelin $ *)
 
 open Formula
 open Sequent
diff --git a/plugins/firstorder/ground.ml b/plugins/firstorder/ground.ml
index 354bcda2..163b9891 100644
--- a/plugins/firstorder/ground.ml
+++ b/plugins/firstorder/ground.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: ground.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
+(* $Id: ground.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
 
 open Formula
 open Sequent
diff --git a/plugins/firstorder/ground.mli b/plugins/firstorder/ground.mli
index ba8051da..8328bb3a 100644
--- a/plugins/firstorder/ground.mli
+++ b/plugins/firstorder/ground.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: ground.mli 13323 2010-07-24 15:57:30Z herbelin $ *)
+(* $Id: ground.mli 14641 2011-11-06 11:59:10Z herbelin $ *)
 
 val ground_tac:     Tacmach.tactic ->
   (Proof_type.goal Tacmach.sigma -> Sequent.t) -> Tacmach.tactic
diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml
index 714604ae..4802aaa3 100644
--- a/plugins/firstorder/instances.ml
+++ b/plugins/firstorder/instances.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        *)
 (************************************************************************)
 
-(*i $Id: instances.ml 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: instances.ml 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 open Formula
 open Sequent
diff --git a/plugins/firstorder/instances.mli b/plugins/firstorder/instances.mli
index 8b913719..537e40e7 100644
--- a/plugins/firstorder/instances.mli
+++ b/plugins/firstorder/instances.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        *)
 (************************************************************************)
 
-(*i $Id: instances.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: instances.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 open Term
 open Tacmach
diff --git a/plugins/firstorder/rules.ml b/plugins/firstorder/rules.ml
index 9cff67dc..e6d73fb6 100644
--- a/plugins/firstorder/rules.ml
+++ b/plugins/firstorder/rules.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: rules.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
+(* $Id: rules.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
 
 open Util
 open Names
diff --git a/plugins/firstorder/rules.mli b/plugins/firstorder/rules.mli
index ec6d2bd0..a5a6b614 100644
--- a/plugins/firstorder/rules.mli
+++ b/plugins/firstorder/rules.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: rules.mli 13323 2010-07-24 15:57:30Z herbelin $ *)
+(* $Id: rules.mli 14641 2011-11-06 11:59:10Z herbelin $ *)
 
 open Term
 open Tacmach
diff --git a/plugins/firstorder/sequent.ml b/plugins/firstorder/sequent.ml
index 1d439693..faac286e 100644
--- a/plugins/firstorder/sequent.ml
+++ b/plugins/firstorder/sequent.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: sequent.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
+(* $Id: sequent.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
 
 open Term
 open Util
diff --git a/plugins/firstorder/sequent.mli b/plugins/firstorder/sequent.mli
index 1232f1e8..ef052605 100644
--- a/plugins/firstorder/sequent.mli
+++ b/plugins/firstorder/sequent.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: sequent.mli 13323 2010-07-24 15:57:30Z herbelin $ *)
+(* $Id: sequent.mli 14641 2011-11-06 11:59:10Z herbelin $ *)
 
 open Term
 open Util
diff --git a/plugins/firstorder/unify.ml b/plugins/firstorder/unify.ml
index 835b0409..4e0ad108 100644
--- a/plugins/firstorder/unify.ml
+++ b/plugins/firstorder/unify.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        *)
 (************************************************************************)
 
-(*i $Id: unify.ml 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: unify.ml 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 open Util
 open Formula
diff --git a/plugins/firstorder/unify.mli b/plugins/firstorder/unify.mli
index af2ce01d..4e0d88d3 100644
--- a/plugins/firstorder/unify.mli
+++ b/plugins/firstorder/unify.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: unify.mli 13323 2010-07-24 15:57:30Z herbelin $ *)
+(* $Id: unify.mli 14641 2011-11-06 11:59:10Z herbelin $ *)
 
 open Term
 
-- 
cgit v1.2.3