]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/cic_omdoc/content.mli
Unuseful id removed from hypothesis.
[helm.git] / helm / ocaml / cic_omdoc / content.mli
index a672cd83cffb8c6176f70511ba6b34c06b5c46fc..fea233da0d2d321511db9a8d74d46a018e339faa 100644 (file)
@@ -138,7 +138,6 @@ type 'term conjecture = id * int * 'term context * 'term
 and 'term context = 'term hypothesis list
 
 and 'term hypothesis =
- id *
  ['term decl_context_element | ('term,'term proof) def_context_element ] option
 ;;