]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/cic_notation/cicNotationFwd.ml
added hyperlinks on case pattern heads and outtype
[helm.git] / helm / ocaml / cic_notation / cicNotationFwd.ml
index 2e5121b92c21e4d5ee4a6694e595c90de7f773de..3ef1ff7e0deada79265cf44c8d6628b231facd5b 100644 (file)
@@ -114,8 +114,8 @@ let instantiate_level2 env term =
   and aux_capture_var env (name, ty_opt) = (aux env name, aux_opt env ty_opt)
   and aux_branch env (pattern, term) =
     (aux_pattern env pattern, aux env term)
-  and aux_pattern env (head, vars) =
-    (head, List.map (aux_capture_var env) vars)
+  and aux_pattern env (head, hrefs, vars) =
+    (head, hrefs, List.map (aux_capture_var env) vars)
   and aux_definition env (var, term, i) =
     (aux_capture_var env var, aux env term, i)
   and aux_substs env substs =