From 164c6861860e6b52818c031f901ffeff91fca16a Mon Sep 17 00:00:00 2001
From: Enrico Tassi <gareuselesinge@debian.org>
Date: Tue, 26 Jan 2016 16:56:33 +0100
Subject: Imported Upstream version 8.5

---
 plugins/quote/Quote.v     | 2 +-
 plugins/quote/g_quote.ml4 | 2 +-
 plugins/quote/quote.ml    | 6 +++---
 3 files changed, 5 insertions(+), 5 deletions(-)

(limited to 'plugins/quote')

diff --git a/plugins/quote/Quote.v b/plugins/quote/Quote.v
index ca1a18e8..2d154adc 100644
--- a/plugins/quote/Quote.v
+++ b/plugins/quote/Quote.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/plugins/quote/g_quote.ml4 b/plugins/quote/g_quote.ml4
index e27fe7f4..fdc5c2bb 100644
--- a/plugins/quote/g_quote.ml4
+++ b/plugins/quote/g_quote.ml4
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/plugins/quote/quote.ml b/plugins/quote/quote.ml
index 2a2ef30f..ff6acf13 100644
--- a/plugins/quote/quote.ml
+++ b/plugins/quote/quote.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -211,9 +211,9 @@ let compute_rhs bodyi index_of_f =
           let i = destRel (Array.last args) in
 	  PMeta (Some (coerce_meta_in i))
       | App (f,args) ->
-          PApp (pi3 (pattern_of_constr (Global.env()) Evd.empty f), Array.map aux args)
+          PApp (pattern_of_constr (Global.env()) Evd.empty f, Array.map aux args)
       | Cast (c,_,_) -> aux c
-      | _ -> pi3 (pattern_of_constr (Global.env())(*FIXME*) Evd.empty c)
+      | _ -> pattern_of_constr (Global.env())(*FIXME*) Evd.empty c
   in
   aux bodyi
 
-- 
cgit v1.2.3