From e0d682ec25282a348d35c5b169abafec48555690 Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Mon, 20 Aug 2012 18:27:01 +0200
Subject: Imported Upstream version 8.4dfsg

---
 plugins/funind/Recdef.v                       | 2 +-
 plugins/funind/functional_principles_types.ml | 6 ------
 plugins/funind/g_indfun.ml4                   | 2 +-
 plugins/funind/invfun.ml                      | 2 +-
 plugins/funind/merge.ml                       | 2 +-
 plugins/funind/recdef.ml                      | 2 +-
 6 files changed, 5 insertions(+), 11 deletions(-)

(limited to 'plugins/funind')

diff --git a/plugins/funind/Recdef.v b/plugins/funind/Recdef.v
index b29b8362..b2955e90 100644
--- a/plugins/funind/Recdef.v
+++ b/plugins/funind/Recdef.v
@@ -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-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index 6df9d574..00e966fb 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -142,12 +142,6 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type =
 (*     observe (str "replacing " ++ pr_lconstr c ++ str " by "  ++ pr_lconstr res); *)
     res
   in
-  let rec has_dummy_var t  =
-    fold_constr
-      (fun b t -> b || (eq_constr t dummy_var) || (has_dummy_var t))
-      false
-      t
-  in
   let rec compute_new_princ_type remove env pre_princ : types*(constr list) =
     let (new_princ_type,_) as res =
       match kind_of_term pre_princ with
diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4
index 06abb8ce..85d79214 100644
--- a/plugins/funind/g_indfun.ml4
+++ b/plugins/funind/g_indfun.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-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index 95ca86c2..55451a9f 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.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-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml
index 4eedf8dc..6ee2f352 100644
--- a/plugins/funind/merge.ml
+++ b/plugins/funind/merge.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-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 3355300e..892c1a77 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.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-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
-- 
cgit v1.2.3