* removed wrong unref

[helm.git] / helm / ocaml / cic_omdoc / content.ml

diff --git a/helm/ocaml/cic_omdoc/content.ml b/helm/ocaml/cic_omdoc/content.ml
index 2f956d7d11a7aa59a026173900808112c38cc6cc..6679cfabb466e35758710a6edeba0f542e9448fa 100644 (file)
--- a/helm/ocaml/cic_omdoc/content.ml
+++ b/helm/ocaml/cic_omdoc/content.ml
@@ -121,8 +121,9 @@ and 'term conclude_item =
        }
 
 and 'term arg =
-         Aux of int
+         Aux of string
        | Premise of premise
+       | Lemma of lemma
        | Term of 'term
        | ArgProof of 'term proof
        | ArgMethod of string (* ???? *)
@@ -133,6 +134,13 @@ and premise =
          premise_binder : string option;
          premise_n : int option;
        }
+
+and lemma =
+       { lemma_id: string;
+         lemma_name: string;
+         lemma_uri: string 
+       }
+
 ;;
  
 type 'term conjecture = id * int * 'term context * 'term
@@ -140,7 +148,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
 ;;