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.

diff --git a/components/cic_disambiguation/disambiguate.ml b/components/cic_disambiguation/disambiguate.ml
index 1560f00160247992ab701c0e1f2243d49ffcd5ab..f3600b7cbc34602ba9e8a433ae853aaf66f4d3b8 100644 (file)
--- a/components/cic_disambiguation/disambiguate.ml
+++ b/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) ->