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

1 files changed, 2 insertions, 1 deletions

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