From c3feef4ed5dec126f1144dec91eee9c0f0522a94 Mon Sep 17 00:00:00 2001
From: Pierre Boutillier
Date: Wed, 2 Apr 2014 11:22:21 +0200
Subject: Fix Bug 3217

Normalize the term to see if there are arguments to daclare implicits only if
at least one argument occurs in the non normal form
---
 library/impargs.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/library/impargs.ml b/library/impargs.ml
index 5ec21a3c92..1bcff86953 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -207,7 +207,8 @@ let add_free_rels_until strict strongly_strict revpat bound env m pos acc =
     | _ ->
         iter_constr_with_full_binders push_lift (frec rig) ed c
   in
-  frec true (env,1) m; acc
+  let () = if not (Vars.noccur_between 1 bound m) then frec true (env,1) m in
+  acc
 
 let rec is_rigid_head t = match kind_of_term t with
   | Rel _ | Evar _ -> false
-- 
cgit v1.2.3