X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_disambiguation%2Fdisambiguate.ml;fp=helm%2Focaml%2Fcic_disambiguation%2Fdisambiguate.ml;h=71f582211f5530a407ae661b8a2c028072e7ab73;hb=727d6939c3f3ff1769ac1d11cad11d2e06433295;hp=f320db2cc3942b18fbbd356cc924f6d204af867a;hpb=9d9c3c7cbed6ea98b10421381d88c4d5a1fbf0f0;p=helm.git

diff --git a/helm/ocaml/cic_disambiguation/disambiguate.ml b/helm/ocaml/cic_disambiguation/disambiguate.ml
index f320db2cc..71f582211 100644
--- a/helm/ocaml/cic_disambiguation/disambiguate.ml
+++ b/helm/ocaml/cic_disambiguation/disambiguate.ml
@@ -118,7 +118,7 @@ let resolve (env: codomain_item Environment.t) (item: domain_item) ?(num = "") ?
       (DisambiguateTypes.string_of_domain_item item))
 
   (* TODO move it to Cic *)
-let find_in_context name (context: Cic.name list) =
+let find_in_context name context =
   let rec aux acc = function
     | [] -> raise Not_found
     | Cic.Name hd :: tl when hd = name -> acc
@@ -683,16 +683,16 @@ 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) ->
+          domain_rev_of_term [] ty @ dom
+        ) (dom @ domain_rev_of_term [] ty) params
+      in
        List.filter
         (fun name->
           not (  List.exists (fun (name',_) -> name = Id name') params
               || List.exists (fun (name',_,_) -> name = Id name') fields)
         ) dom
-      in
-       List.fold_left
-        (fun dom (_,ty) ->
-          domain_rev_of_term [] ty @ dom
-        ) (dom @ domain_rev_of_term [] ty) params
  in
   rev_uniq domain_rev