X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fdisambiguation%2Fdisambiguate.ml;h=f27c723b0692eceb453084b52e47fd25758d66dd;hb=19a25bf176255055193372554437729a6fa1894c;hp=4476d562a949d0e9a82e0bc69f49dfb8dacc3649;hpb=46ee64f692a1e5e65864ebb82ec875e8d115843c;p=helm.git

diff --git a/matita/components/disambiguation/disambiguate.ml b/matita/components/disambiguation/disambiguate.ml
index 4476d562a..f27c723b0 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,15 +303,19 @@ 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
-   | Ast.Theorem (_,_,ty,bo,_) ->
+   | Ast.Theorem (_,ty,bo,_) ->
       domain_of_term [] ty
       @ (match bo with
           None -> []
         | Some bo -> domain_of_term [] bo)
-   | Ast.Inductive (params,tyl) ->
+   | Ast.Inductive (params,tyl,_) ->
       let context, dom = 
        List.fold_left
         (fun (context, dom) (var, ty) ->
@@ -359,7 +335,7 @@ let domain_of_obj ~context ast =
                List.map
                 (fun (_,ty) -> domain_of_term context_w_types ty) cl))
                 tyl)
-   | Ast.Record (params,var,ty,fields) ->
+   | Ast.Record (params,var,ty,fields,_) ->
       let context, dom = 
        List.fold_left
         (fun (context, dom) (var, ty) ->
@@ -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)