Remove non-DFSG contentsupstream/8.4_gamma0+really8.4beta2+dfsg

1 files changed, 6 insertions, 7 deletions

diff --git a/library/impargs.ml b/library/impargs.ml
index ef7f5921..73699a90 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -207,11 +207,10 @@ let rec is_rigid_head t = match kind_of_term t with
 
 (* calcule la liste des arguments implicites *)
 
-let find_displayed_name_in all avoid na b =
-  if all then
-    compute_and_force_displayed_name_in (RenamingElsewhereFor b) avoid na b
-  else
-    compute_displayed_name_in (RenamingElsewhereFor b) avoid na b
+let find_displayed_name_in all avoid na (_,b as envnames_b) =
+  let flag = RenamingElsewhereFor envnames_b in
+  if all then compute_and_force_displayed_name_in flag avoid na b
+  else compute_displayed_name_in flag avoid na b
 
 let compute_implicits_gen strict strongly_strict revpat contextual all env t =
   let rigid = ref true in
@@ -219,7 +218,7 @@ let compute_implicits_gen strict strongly_strict revpat contextual all env t =
     let t = whd_betadeltaiota env t in
     match kind_of_term t with
       | Prod (na,a,b) ->
-	  let na',avoid' = find_displayed_name_in all avoid na b in
+	  let na',avoid' = find_displayed_name_in all avoid na (names,b) in
 	  add_free_rels_until strict strongly_strict revpat n env a (Hyp (n+1))
             (aux (push_rel (na',None,a) env) avoid' (n+1) (na'::names) b)
       | _ ->
@@ -232,7 +231,7 @@ let compute_implicits_gen strict strongly_strict revpat contextual all env t =
   in
   match kind_of_term (whd_betadeltaiota env t) with
     | Prod (na,a,b) ->
-	let na',avoid = find_displayed_name_in all [] na b in
+	let na',avoid = find_displayed_name_in all [] na ([],b) in
 	let v = aux (push_rel (na',None,a) env) avoid 1 [na'] b in
 	!rigid, Array.to_list v
     | _ -> true, []