X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fdisambiguation%2Fdisambiguate.ml;h=58e600a425e6af9bbf437aa57e42e2f7afa9a11b;hb=53b8e2af661ad4165aa0b1deccd0a7522d96ce2e;hp=95d6082d0b4296bd1ee12d7649cb8b0c11122ab4;hpb=f7da48c844105a52a705872dfa0d4104de010c82;p=helm.git

diff --git a/matita/components/disambiguation/disambiguate.ml b/matita/components/disambiguation/disambiguate.ml
index 95d6082d0..58e600a42 100644
--- a/matita/components/disambiguation/disambiguate.ml
+++ b/matita/components/disambiguation/disambiguate.ml
@@ -261,34 +261,6 @@ let rec domain_of_term ?(loc = HExtlib.dummy_floc) ~context = function
       let where_dom =
         domain_of_term ~loc ~context:(string_of_name var :: context) where in
       body_dom @ type_dom @ where_dom
-  | Ast.LetRec (kind, defs, where) ->
-      let add_defs context =
-        List.fold_left
-          (fun acc (_, (var, _), _, _) -> string_of_name var :: acc
-          ) context defs in
-      let where_dom = domain_of_term ~loc ~context:(add_defs context) where in
-      let defs_dom =
-        List.fold_left
-          (fun dom (params, (_, typ), body, _) ->
-            let context' =
-             add_defs
-              (List.fold_left
-                (fun acc (var,_) -> string_of_name var :: acc)
-                context params)
-            in
-            List.rev
-             (snd
-               (List.fold_left
-                (fun (context,res) (var,ty) ->
-                  string_of_name var :: context,
-                  domain_of_term_option ~loc ~context ty @ res)
-                (add_defs context,[]) params))
-            @ dom
-            @ domain_of_term_option ~loc ~context:context' typ
-            @ domain_of_term ~loc ~context:context' body
-          ) [] defs
-      in
-      defs_dom @ where_dom
   | Ast.Ident (name, subst) ->
       (try
         (* the next line can raise Not_found *)
@@ -331,6 +303,10 @@ and domain_of_term_option ~loc ~context = function
 let domain_of_term ~context term = 
  uniq_domain (domain_of_term ~context term)
 
+let domain_of_term_option ~context = function
+   | None      -> []
+   | Some term -> domain_of_term ~context term
+
 let domain_of_obj ~context ast =
  assert (context = []);
   match ast with
@@ -376,6 +352,33 @@ let domain_of_obj ~context ast =
           (fun (context,res) (name,ty,_,_) ->
             Some name::context, res @ domain_of_term context ty
           ) (context_w_types,[]) fields)
+   | Ast.LetRec (kind, defs, _) ->
+       let add_defs context =
+         List.fold_left
+           (fun acc (_, (var, _), _, _) -> string_of_name var :: acc
+           ) context defs in
+       let defs_dom =
+         List.fold_left
+           (fun dom (params, (_, typ), body, _) ->
+             let context' =
+              add_defs
+               (List.fold_left
+                 (fun acc (var,_) -> string_of_name var :: acc)
+                 context params)
+             in
+             List.rev
+              (snd
+                (List.fold_left
+                 (fun (context,res) (var,ty) ->
+                   string_of_name var :: context,
+                   domain_of_term_option ~context ty @ res)
+                 (add_defs context,[]) params))
+             @ dom
+             @ domain_of_term_option ~context:context' typ
+             @ domain_of_term ~context:context' body
+           ) [] defs
+      in
+      defs_dom
 
 let domain_of_obj ~context obj = 
  uniq_domain (domain_of_obj ~context obj)