The Aux argument of conclude is now of type string (used to be int).

[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 be46f59610aa34341c245a6d626592d9fa8a456b..a09e25cf2b3b46323192d4744e28fcaa95be7d4a 100644 (file)
--- a/helm/ocaml/cic_omdoc/content.ml
+++ b/helm/ocaml/cic_omdoc/content.ml
@@ -34,7 +34,7 @@
 
 type id = string;;
 type joint_recursion_kind =
- [ `Recursive
+ [ `Recursive of int list
  | `CoRecursive
  | `Inductive of int    (* paramsno *)
  | `CoInductive of int  (* paramsno *)
@@ -121,7 +121,7 @@ and 'term conclude_item =
        }
 
 and 'term arg =
-         Aux of int
+         Aux of string
        | Premise of premise
        | Term of 'term
        | ArgProof of 'term proof