X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fcontent%2FnotationUtil.ml;h=823febdb6c31c61e12cc2cc3a65d47f90fc55541;hb=53b8e2af661ad4165aa0b1deccd0a7522d96ce2e;hp=3d80e8fd51427a0d091335a95e186b1b4553d91f;hpb=d4f2d4c1a4784f84aa27e1bb96b8b377a6553c65;p=helm.git

diff --git a/matita/components/content/notationUtil.ml b/matita/components/content/notationUtil.ml
index 3d80e8fd5..823febdb6 100644
--- a/matita/components/content/notationUtil.ml
+++ b/matita/components/content/notationUtil.ml
@@ -43,15 +43,6 @@ let visit_ast ?(special_k = fun _ -> assert false)
     | Ast.Cast (t1, t2) -> Ast.Cast (k t1, k t2)
     | Ast.LetIn (var, t1, t3) ->
         Ast.LetIn (aux_capture_variable var, k t1, k t3)
-    | Ast.LetRec (kind, definitions, term) ->
-        let definitions =
-          List.map
-            (fun (params, var, ty, decrno) ->
-              List.map aux_capture_variable params, aux_capture_variable var,
-              k ty, decrno)
-            definitions
-        in
-        Ast.LetRec (kind, definitions, k term)
     | Ast.Ident (name, Some substs) ->
         Ast.Ident (name, Some (aux_substs substs))
     | Ast.Uri (name, Some substs) -> Ast.Uri (name, Some (aux_substs substs))
@@ -202,9 +193,6 @@ let meta_names_of_term term =
     | Ast.LetIn (_, t1, t3) ->
         aux t1 ;
         aux t3
-    | Ast.LetRec (_, definitions, body) ->
-        List.iter aux_definition definitions ;
-        aux body
     | Ast.Uri (_, Some substs) -> aux_substs substs
     | Ast.Ident (_, Some substs) -> aux_substs substs
     | Ast.Meta (_, substs) -> aux_meta_substs substs
@@ -232,10 +220,6 @@ let meta_names_of_term term =
    function
       Ast.Pattern (head, _, vars) -> List.iter aux_capture_var vars
     | Ast.Wildcard -> ()
-  and aux_definition (params, var, term, decrno) =
-    List.iter aux_capture_var params ;
-    aux_capture_var var ;
-    aux term
   and aux_substs substs = List.iter (fun (_, term) -> aux term) substs
   and aux_meta_substs meta_substs = List.iter aux_opt meta_substs
   and aux_variable = function
@@ -351,7 +335,7 @@ let fresh_id () =
   !fresh_index
 
   (* TODO ensure that names generated by fresh_var do not clash with user's *)
-  (* FG: "η" is not an identifier (it is rendered, but not be parsed) *)
+  (* FG: "η" is not an identifier (it is rendered, but not parsed) *)
 let fresh_name () = "eta" ^ string_of_int (fresh_id ())
 
 let rec freshen_term ?(index = ref 0) term =
@@ -375,9 +359,8 @@ let freshen_obj obj =
   let freshen_term = freshen_term ~index in
   let freshen_name_ty = List.map (fun (n, t) -> (n, freshen_term t)) in
   let freshen_name_ty_b = List.map (fun (n,t,b,i) -> (n,freshen_term t,b,i)) in
-  let freshen_capture_variables =
-   List.map (fun (n,t) -> (freshen_term n, HExtlib.map_option freshen_term t))
-  in
+  let freshen_capture_variable (n, t) = freshen_term n, HExtlib.map_option freshen_term t in 
+  let freshen_capture_variables = List.map freshen_capture_variable in
   match obj with
   | NotationPt.Inductive (params, indtypes) ->
       let indtypes =
@@ -386,14 +369,23 @@ let freshen_obj obj =
           indtypes
       in
       NotationPt.Inductive (freshen_capture_variables params, indtypes)
-  | NotationPt.Theorem (flav, n, t, ty_opt,p) ->
+  | NotationPt.Theorem (n, t, ty_opt, attrs) ->
       let ty_opt =
         match ty_opt with None -> None | Some ty -> Some (freshen_term ty)
       in
-      NotationPt.Theorem (flav, n, freshen_term t, ty_opt,p)
+      NotationPt.Theorem (n, freshen_term t, ty_opt, attrs)
   | NotationPt.Record (params, n, ty, fields) ->
       NotationPt.Record (freshen_capture_variables params, n,
         freshen_term ty, freshen_name_ty_b fields)
+  | NotationPt.LetRec (kind, definitions, attrs) ->
+      let definitions =
+        List.map
+          (fun (params, var, ty, decrno) ->
+            freshen_capture_variables params, freshen_capture_variable var,
+            freshen_term ty, decrno)
+          definitions
+      in
+      NotationPt.LetRec (kind, definitions, attrs)
 
 let freshen_term = freshen_term ?index:None