From 109c90efd0dd2bfbeb6c29b263ccd9b2e84e5b9e Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Mon, 25 Aug 2014 21:46:26 +0200
Subject: Fixing bug #3377 by giving env and sigma to constrMathching. Now it's
 possible to match on a primitive projection application c.(p) using "?f _",
 binding f to (fun x => x.(p)) with the correct typing.

---
 plugins/quote/quote.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins')

diff --git a/plugins/quote/quote.ml b/plugins/quote/quote.ml
index ea459e551f..7ed4a0dbcd 100644
--- a/plugins/quote/quote.ml
+++ b/plugins/quote/quote.ml
@@ -401,7 +401,7 @@ let quote_terms ivs lc =
       match l with
         | (lhs, rhs)::tail ->
             begin try
-              let s1 = Id.Map.bindings (matches rhs c) in
+              let s1 = Id.Map.bindings (matches (Global.env ()) Evd.empty rhs c) in
               let s2 = List.map (fun (i,c_i) -> (coerce_meta_out i,aux c_i)) s1
 	      in
               Termops.subst_meta s2 lhs
-- 
cgit v1.2.3