]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/cic_notation/cicNotationUtil.ml
added hyperlinks on case pattern heads and outtype
[helm.git] / helm / ocaml / cic_notation / cicNotationUtil.ml
index 29edf6e7cb6354de9f4587cf360eed2473bdd384..426846877617a054fade73112c31944aaf03673f 100644 (file)
@@ -63,8 +63,8 @@ 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, vars), term) =
-    ((head, List.map aux_capture_variable vars), k term)
+  and aux_pattern ((head, hrefs, vars), term) =
+    ((head, hrefs, List.map aux_capture_variable vars), k term)
   and aux_subst (name, term) = (name, k term)
   and aux_substs substs = List.map aux_subst substs
   in
@@ -203,7 +203,7 @@ let meta_names_of_term term =
   and aux_branch (pattern, term) =
     aux_pattern pattern ;
     aux term
-  and aux_pattern (head, vars) = 
+  and aux_pattern (head, _, vars) = 
     List.iter aux_capture_var vars
   and aux_definition (var, term, i) =
     aux_capture_var var ;