From 61dc740ed1c3780cccaec00d059a28f0d31d0052 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Mon, 4 Jun 2012 12:07:52 +0200 Subject: Imported Upstream version 8.4~gamma0+really8.4beta2 --- library/impargs.ml | 13 ++++++------- 1 file changed, 6 insertions(+), 7 deletions(-) (limited to 'library/impargs.ml') 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, [] -- cgit v1.2.3