From 2d3916766d3f145643a994aa83174c98394d5baa Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Tue, 3 Mar 2015 21:45:42 +0100
Subject: Fix bug #3590, keeping evars that are not turned into named metas by
 pattern_of_constr in an evar_map, as they can appear in the context of said
 named metas, which is used by change. Not sure what to do in the PEvar case,
 which never matches anyway according to Constr_matching.matches.

---
 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 637e0e28d5..2a2ef30fb1 100644
--- a/plugins/quote/quote.ml
+++ b/plugins/quote/quote.ml
@@ -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 (snd (pattern_of_constr (Global.env()) Evd.empty f), Array.map aux args)
+          PApp (pi3 (pattern_of_constr (Global.env()) Evd.empty f), Array.map aux args)
       | Cast (c,_,_) -> aux c
-      | _ -> snd (pattern_of_constr (Global.env())(*FIXME*) Evd.empty c)
+      | _ -> pi3 (pattern_of_constr (Global.env())(*FIXME*) Evd.empty c)
   in
   aux bodyi
 
-- 
cgit v1.2.3