added hyperlinks on case pattern heads and outtype

[helm.git] / helm / ocaml / cic_disambiguation / disambiguate.ml

diff --git a/helm/ocaml/cic_disambiguation/disambiguate.ml b/helm/ocaml/cic_disambiguation/disambiguate.ml
index 58927e53b887d8b7aeddfe9e82c4a6e85a7bbc7b..5096789d964eccc1560d05fe46ce68d92c4846c7 100644 (file)
--- a/helm/ocaml/cic_disambiguation/disambiguate.ml
+++ b/helm/ocaml/cic_disambiguation/disambiguate.ml
@@ -134,7 +134,7 @@ let interpretate_term ~(context: Cic.name list) ~env ~uri ~is_path ast =
     | CicNotationPt.Case (term, indty_ident, outtype, branches) ->
         let cic_term = aux loc context term in
         let cic_outtype = aux_option loc context None outtype in
-        let do_branch ((head, args), term) =
+        let do_branch ((head, _, args), term) =
           let rec do_branch' context = function
             | [] -> aux loc context term
             | (name, typ) :: tl ->
@@ -151,7 +151,7 @@ let interpretate_term ~(context: Cic.name list) ~env ~uri ~is_path ast =
         in
         let (indtype_uri, indtype_no) =
           match indty_ident with
-          | Some indty_ident ->
+          | Some (indty_ident, _) ->
               (match resolve env (Id indty_ident) () with
               | Cic.MutInd (uri, tyno, _) -> (uri, tyno)
               | Cic.Implicit _ -> raise Try_again
@@ -159,7 +159,7 @@ let interpretate_term ~(context: Cic.name list) ~env ~uri ~is_path ast =
           | None ->
               let fst_constructor =
                 match branches with
-                | ((head, _), _) :: _ -> head
+                | ((head, _, _), _) :: _ -> head
                 | [] -> raise Invalid_choice
               in
               (match resolve env (Id fst_constructor) () with
@@ -485,9 +485,9 @@ let rec domain_rev_of_term ?(loc = dummy_floc) context = function
       let outtype_dom = domain_rev_of_term_option loc context outtype in
       let get_first_constructor = function
         | [] -> []
-        | ((head, _), _) :: _ -> [ Id head ]
+        | ((head, _, _), _) :: _ -> [ Id head ]
       in
-      let do_branch ((head, args), term) =
+      let do_branch ((head, _, args), term) =
         let (term_context, args_domain) =
           List.fold_left
             (fun (cont, dom) (name, typ) ->
@@ -505,7 +505,7 @@ let rec domain_rev_of_term ?(loc = dummy_floc) context = function
       branches_dom @ outtype_dom @ term_dom @
       (match indty_ident with
        | None -> get_first_constructor branches
-       | Some ident -> [ Id ident ])
+       | Some (ident, _) -> [ Id ident ])
   | CicNotationPt.Cast (term, ty) ->
       let term_dom = domain_rev_of_term ~loc context term in
       let ty_dom = domain_rev_of_term ~loc context ty in