X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_transformations%2FapplyTransformation.mli;h=8e023aea626f366cbfdc7cdf6778fa01f5854903;hb=97c2d258a5c524eb5c4b85208899d80751a2c82f;hp=4642cc67d37fde2c2beac7b568e0d75a62a8c402;hpb=ff981d975589f8d21a364e7cfe875647f7483cd9;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 *)