From fdad03c5c247ab6cfdde8fd58658d9e40a3fd8aa Mon Sep 17 00:00:00 2001
From: herbelin
Date: Thu, 24 Dec 2009 11:05:43 +0000
Subject: In "simpl c" and "change c with d", c can be a pattern.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12608 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 plugins/quote/quote.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'plugins')

diff --git a/plugins/quote/quote.ml b/plugins/quote/quote.ml
index e1a16ce498..2e4d07d633 100644
--- a/plugins/quote/quote.ml
+++ b/plugins/quote/quote.ml
@@ -215,9 +215,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 (pattern_of_constr Evd.empty f, Array.map aux args)
+          PApp (snd (pattern_of_constr Evd.empty f), Array.map aux args)
       | Cast (c,_,_) -> aux c
-      | _ -> pattern_of_constr Evd.empty c
+      | _ -> snd (pattern_of_constr Evd.empty c)
   in
   aux bodyi
 
-- 
cgit v1.2.3