X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Facic_content%2FcicNotationUtil.ml;h=99aafa44051765813c6f198ad71cd7945a626cbc;hb=70c83bce7d1d50c19c297e47691f7d66208e4d83;hp=f331b79ca8d2da4c3a545c54b6789dcb1eb59a7b;hpb=774c8d18f41e71ae7e26a90d726d10a6f95de1fe;p=helm.git diff --git a/helm/software/components/acic_content/cicNotationUtil.ml b/helm/software/components/acic_content/cicNotationUtil.ml index f331b79ca..99aafa440 100644 --- a/helm/software/components/acic_content/cicNotationUtil.ml +++ b/helm/software/components/acic_content/cicNotationUtil.ml @@ -67,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 @@ -213,8 +216,10 @@ 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_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 ;