From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Sun, 5 Nov 2006 16:19:38 +0000 (+0000)
Subject: Bug fixed: the disambiguation domain for a record with left parameters was
X-Git-Tag: 0.4.95@7852~820
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=3cfd4bb3d93b84b4b59ac04265ec00e5f5253c02;p=helm.git

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 1560f0016..f3600b7cb 100644
--- 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) ->