Unuseful id removed from hypothesis.

[helm.git] / helm / ocaml / cic_transformations / content2pres.ml

diff --git a/helm/ocaml/cic_transformations/content2pres.ml b/helm/ocaml/cic_transformations/content2pres.ml
index 9a5ad74fd9f6d954eb1202f04ac3b7f75be6fc29..cfa061bfb2e442c93da5457d2fa7545ccf444edc 100644 (file)
--- a/helm/ocaml/cic_transformations/content2pres.ml
+++ b/helm/ocaml/cic_transformations/content2pres.ml
@@ -810,13 +810,13 @@ let content2pres term2pres (id,params,metasenv,obj) =
                            (P.Mrow [Some "helm", "xref", id]
                              (List.map
                                (function
-                                   (_,None) ->
+                                   None ->
                                      P.Mrow []
                                       [ P.Mi [] "_" ;
                                         P.Mo [] ":?" ;
                                         P.Mi [] "_"]
-                                 | (_,Some (`Declaration d))
-                                 | (_,Some (`Hypothesis d)) ->
+                                 | Some (`Declaration d)
+                                 | Some (`Hypothesis d) ->
                                     let
                                      { K.dec_name = dec_name ;
                                        K.dec_type = ty } = d
@@ -828,7 +828,7 @@ let content2pres term2pres (id,params,metasenv,obj) =
                                             | Some n -> n) ;
                                          P.Mo [] ":" ;
                                          term2pres ty]
-                                 | (_,Some (`Definition d)) ->
+                                 | Some (`Definition d) ->
                                     let
                                      { K.def_name = def_name ;
                                        K.def_term = bo } = d
@@ -840,7 +840,7 @@ let content2pres term2pres (id,params,metasenv,obj) =
                                             | Some n -> n) ;
                                          P.Mo [] ":=" ;
                                          term2pres bo]
-                                 | (_,Some (`Proof p)) ->
+                                 | Some (`Proof p) ->
                                     let proof_name = p.K.proof_name in
                                      P.Mrow []
                                       [ P.Mi []