From 5cb3f5cf0571c537b3c14cf9220fe58562da4f0c Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Sun, 5 Nov 2006 16:19:38 +0000 Subject: [PATCH] Bug fixed: the disambiguation domain for a record with left parameters was not obtained with a pre-visit. The result was that often Failures were detected later than possible with consequent waste of time. --- .../components/cic_disambiguation/disambiguate.ml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/helm/software/components/cic_disambiguation/disambiguate.ml b/helm/software/components/cic_disambiguation/disambiguate.ml index 1560f0016..f3600b7cb 100644 --- a/helm/software/components/cic_disambiguation/disambiguate.ml +++ b/helm/software/components/cic_disambiguation/disambiguate.ml @@ -727,12 +727,12 @@ let domain_of_obj ~context ast = List.flatten (List.rev_map (fun (_,ty,_,_) -> domain_rev_of_term [] ty) fields) in let dom = - List.fold_left - (fun dom (_,ty) -> + List.fold_right + (fun (_,ty) dom -> match ty with None -> dom - | Some ty -> domain_rev_of_term [] ty @ dom - ) (dom @ domain_rev_of_term [] ty) params + | Some ty -> dom @ domain_rev_of_term [] ty + ) params (dom @ domain_rev_of_term [] ty) in List.filter (fun (_,name) -> -- 2.39.2