From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Mon, 11 Jul 2005 14:03:52 +0000 (+0000)
Subject: Bug fixed: the left parameters of a record or inductive type were not added to
X-Git-Tag: pre_notation~47
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=16afd8c4c5e3aa63c466489956c4b1975b25854d;p=helm.git

Bug fixed: the left parameters of a record or inductive type were not added to
the disambiguation domain.
---

diff --git a/helm/ocaml/cic_disambiguation/disambiguate.ml b/helm/ocaml/cic_disambiguation/disambiguate.ml
index dd915a282..6848338c3 100644
--- a/helm/ocaml/cic_disambiguation/disambiguate.ml
+++ b/helm/ocaml/cic_disambiguation/disambiguate.ml
@@ -561,7 +561,12 @@ let domain_of_obj ~context ast =
            List.flatten (
             List.rev_map
              (fun (_,ty) -> domain_rev_of_term [] ty) cl) @
-            domain_rev_of_term [] ty) tyl)
+            domain_rev_of_term [] ty) tyl) in
+      let dom = 
+       List.fold_left
+        (fun dom (_,ty) ->
+          domain_rev_of_term [] ty @ dom
+        ) dom params
       in
        List.filter
         (fun name ->
@@ -572,14 +577,17 @@ let domain_of_obj ~context ast =
       let dom =
        List.flatten
         (List.rev_map (fun (_,ty) -> domain_rev_of_term [] ty) fields) in
-      let dom' =
+      let dom =
        List.filter
         (fun name->
           not (  List.exists (fun (name',_) -> name = Id name') params
               || List.exists (fun (name',_) -> name = Id name') fields)
         ) dom
       in
-       dom' @ domain_rev_of_term [] ty
+       List.fold_left
+        (fun dom (_,ty) ->
+          domain_rev_of_term [] ty @ dom
+        ) (dom @ domain_rev_of_term [] ty) params
  in
   rev_uniq domain_rev