]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/cic_transformations/applyTransformation.mli
ocaml 3.09 transition
[helm.git] / helm / ocaml / cic_transformations / applyTransformation.mli
index 4642cc67d37fde2c2beac7b568e0d75a62a8c402..8e023aea626f366cbfdc7cdf6778fa01f5854903 100644 (file)
@@ -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 *)