X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_transformations%2FapplyTransformation.mli;h=8e023aea626f366cbfdc7cdf6778fa01f5854903;hb=13d6baa55139729871604c0c3f70a70077ba85ca;hp=4642cc67d37fde2c2beac7b568e0d75a62a8c402;hpb=081cb0ae54c7e5babdedeea7559d667183a38638;p=helm.git

diff --git a/helm/ocaml/cic_transformations/applyTransformation.mli b/helm/ocaml/cic_transformations/applyTransformation.mli
index 4642cc67d..8e023aea6 100644
--- a/helm/ocaml/cic_transformations/applyTransformation.mli
+++ b/helm/ocaml/cic_transformations/applyTransformation.mli
@@ -37,6 +37,7 @@ val mml_of_cic_sequent:
  Cic.metasenv ->                              (* metasenv *)
  Cic.conjecture ->                            (* sequent *)
   Gdome.document *                              (* Math ML *)
+   Cic.conjecture *                             (* unshared sequent *)
    (Cic.annconjecture *                         (* annsequent *)
     ((Cic.id, Cic.term) Hashtbl.t *             (* id -> term *)
      (Cic.id, Cic.id option) Hashtbl.t *        (* id -> father id *)