X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_omdoc%2Fcontent.mli;h=fea233da0d2d321511db9a8d74d46a018e339faa;hb=962cc970cd9a2161f69b70aa01b6ee9e289d9778;hp=b58b84b54c62b611fe3161a5b14e1f651f9cc043;hpb=4bcd14a9ed245ccae631697a05ff5a377c02b179;p=helm.git

diff --git a/helm/ocaml/cic_omdoc/content.mli b/helm/ocaml/cic_omdoc/content.mli
index b58b84b54..fea233da0 100644
--- a/helm/ocaml/cic_omdoc/content.mli
+++ b/helm/ocaml/cic_omdoc/content.mli
@@ -25,7 +25,7 @@
 
 type id = string;;
 type joint_recursion_kind =
- [ `Recursive
+ [ `Recursive of int list (* decreasing arguments *)
  | `CoRecursive
  | `Inductive of int    (* paramsno *)
  | `CoInductive of int  (* paramsno *)
@@ -112,8 +112,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 (* ???? *)
@@ -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
@@ -131,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
 ;;