From a0116bdcb169ebe6e891a7bb3b9e642b9082a0a7 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 7 Feb 2019 16:24:32 +0100
Subject: Fix #9508: Unexpected interaction between implicit arguments and
 primitive projections.

This was due to an involuntary capture of a variable name.
---
 interp/impargs.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'interp')

diff --git a/interp/impargs.ml b/interp/impargs.ml
index 959455dfd2..7e8f2f4f3d 100644
--- a/interp/impargs.ml
+++ b/interp/impargs.ml
@@ -200,7 +200,7 @@ let add_free_rels_until strict strongly_strict revpat bound env sigma m pos acc
     | App (f,_) when rig && is_flexible_reference env sigma bound depth f ->
 	if strict then () else
           iter_with_full_binders sigma push_lift (frec false) ed c
-    | Proj (p,c) when rig ->
+    | Proj (p, _) when rig ->
       if strict then () else
         iter_with_full_binders sigma push_lift (frec false) ed c
     | Case _ when rig ->
-- 
cgit v1.2.3