X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fcomponents%2Facic_content%2FcicNotationUtil.ml;h=99aafa44051765813c6f198ad71cd7945a626cbc;hb=87bdd061d096c836a02c77aa26e80d9c36180fad;hp=d9114b1808b1b5cca3da1736977718953b8adc57;hpb=abd2098b6c4a40b36bb4b950c607eb4b4a7852bc;p=helm.git

diff --git a/helm/software/components/acic_content/cicNotationUtil.ml b/helm/software/components/acic_content/cicNotationUtil.ml
index d9114b180..99aafa440 100644
--- a/helm/software/components/acic_content/cicNotationUtil.ml
+++ b/helm/software/components/acic_content/cicNotationUtil.ml
@@ -40,7 +40,9 @@ let visit_ast ?(special_k = fun _ -> assert false) k =
     | Ast.LetRec (kind, definitions, term) ->
         let definitions =
           List.map
-            (fun (var, ty, n) -> aux_capture_variable var, k ty, n)
+            (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)
@@ -65,8 +67,11 @@ let visit_ast ?(special_k = fun _ -> assert false) k =
     | Some term -> Some (k term)
   and aux_capture_variable (term, typ_opt) = k term, aux_opt typ_opt
   and aux_patterns patterns = List.map aux_pattern patterns
-  and aux_pattern ((head, hrefs, vars), term) =
-    ((head, hrefs, List.map aux_capture_variable vars), k term)
+  and aux_pattern =
+   function
+      Ast.Pattern (head, hrefs, vars), term ->
+        Ast.Pattern (head, hrefs, List.map aux_capture_variable vars), k term
+    | Ast.Wildcard, term -> Ast.Wildcard, k term
   and aux_subst (name, term) = (name, k term)
   and aux_substs substs = List.map aux_subst substs
   in
@@ -211,9 +216,12 @@ let meta_names_of_term term =
   and aux_branch (pattern, term) =
     aux_pattern pattern ;
     aux term
-  and aux_pattern (head, _, vars) = 
-    List.iter aux_capture_var vars
-  and aux_definition (var, term, i) =
+  and aux_pattern =
+   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
@@ -367,6 +375,9 @@ 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
   match obj with
   | CicNotationPt.Inductive (params, indtypes) ->
       let indtypes =
@@ -374,15 +385,15 @@ let freshen_obj obj =
           (fun (n, co, ty, ctors) -> (n, co, ty, freshen_name_ty ctors))
           indtypes
       in
-      CicNotationPt.Inductive (freshen_name_ty params, indtypes)
+      CicNotationPt.Inductive (freshen_capture_variables params, indtypes)
   | CicNotationPt.Theorem (flav, n, t, ty_opt) ->
       let ty_opt =
         match ty_opt with None -> None | Some ty -> Some (freshen_term ty)
       in
       CicNotationPt.Theorem (flav, n, freshen_term t, ty_opt)
   | CicNotationPt.Record (params, n, ty, fields) ->
-      CicNotationPt.Record (freshen_name_ty params, n, freshen_term ty,
-        freshen_name_ty_b fields)
+      CicNotationPt.Record (freshen_capture_variables params, n,
+        freshen_term ty, freshen_name_ty_b fields)
 
 let freshen_term = freshen_term ?index:None