X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_omdoc%2Fcontent.mli;h=a672cd83cffb8c6176f70511ba6b34c06b5c46fc;hb=414dc18cdbc1f431758cfce79b0b7827e2419d39;hp=813a31053df36cbccca8dda5f1fbb5633ea86313;hpb=22a8ad8462e81ad68d8016a009fa8003bd52a66f;p=helm.git

diff --git a/helm/ocaml/cic_omdoc/content.mli b/helm/ocaml/cic_omdoc/content.mli
index 813a31053..a672cd83c 100644
--- a/helm/ocaml/cic_omdoc/content.mli
+++ b/helm/ocaml/cic_omdoc/content.mli
@@ -114,6 +114,7 @@ and 'term conclude_item =
 and 'term arg =
          Aux of string
        | Premise of premise
+       | Lemma of lemma
        | Term of 'term
        | ArgProof of 'term proof
        | ArgMethod of string (* ???? *)
@@ -124,6 +125,12 @@ 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