From 84544396cbbf34848be2240acf181b4d5f1f42d2 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Sat, 27 Sep 2014 16:08:02 +0200
Subject: Add a boolean to indicate the unfolding state of a primitive
 projection, so as to reproduce correctly the reduction behavior of existing
 projections, i.e. delta + iota. Make [projection] an abstract datatype in
 Names.ml, most of the patch is about using that abstraction. Fix
 unification.ml which tried canonical projections too early in presence of
 primitive projections.

---
 plugins/quote/quote.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'plugins/quote')

diff --git a/plugins/quote/quote.ml b/plugins/quote/quote.ml
index 745e190cb8..ed7f180014 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 Evd.empty f), Array.map aux args)
+          PApp (snd (pattern_of_constr (Global.env()) Evd.empty f), Array.map aux args)
       | Cast (c,_,_) -> aux c
-      | _ -> snd (pattern_of_constr Evd.empty c)
+      | _ -> snd (pattern_of_constr (Global.env())(*FIXME*) Evd.empty c)
   in
   aux bodyi
 
-- 
cgit v1.2.3