X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_omdoc%2Fcic2acic.mli;h=e6379283d61f98b173154cd4d256e08a70a667f0;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=b5a194951abd8871f5b2a4a640ccd3f2c08350f3;hpb=5c9e1997848c2f74297a5a243679f4bcb6ae0dc7;p=helm.git

diff --git a/helm/ocaml/cic_omdoc/cic2acic.mli b/helm/ocaml/cic_omdoc/cic2acic.mli
index b5a194951..e6379283d 100644
--- a/helm/ocaml/cic_omdoc/cic2acic.mli
+++ b/helm/ocaml/cic_omdoc/cic2acic.mli
@@ -40,21 +40,22 @@ val sort_of_sort: Cic.sort -> sort_kind
 val acic_object_of_cic_object :
   ?eta_fix: bool ->                       (* perform eta_fixing; default: true*)
   Cic.obj ->                              (* object *)
-   Cic.annobj *                           (* annotated object *)
-    (Cic.id, Cic.term) Hashtbl.t *        (* ids_to_terms *)
-    (Cic.id, Cic.id option) Hashtbl.t *   (* ids_to_father_ids *)
-    (Cic.id, sort_kind) Hashtbl.t *       (* ids_to_inner_sorts *)
-    (Cic.id, anntypes) Hashtbl.t *        (* ids_to_inner_types *)
-    (Cic.id, Cic.conjecture) Hashtbl.t *  (* ids_to_conjectures *)
-    (Cic.id, Cic.hypothesis) Hashtbl.t    (* ids_to_hypotheses *)
+   Cic.annobj *                            (* annotated object *)
+    (Cic.id, Cic.term) Hashtbl.t *         (* ids_to_terms *)
+    (Cic.id, Cic.id option) Hashtbl.t *    (* ids_to_father_ids *)
+    (Cic.id, sort_kind) Hashtbl.t *        (* ids_to_inner_sorts *)
+    (Cic.id, anntypes) Hashtbl.t *         (* ids_to_inner_types *)
+    (Cic.id, Cic.conjecture) Hashtbl.t *   (* ids_to_conjectures *)
+    (Cic.id, Cic.hypothesis) Hashtbl.t     (* ids_to_hypotheses *)
 
 val asequent_of_sequent :
   Cic.metasenv ->                         (* metasenv *)
-   Cic.conjecture ->                      (* conjecture *)
-    Cic.annconjecture *                   (* annotated conjecture *)
-    (Cic.id, Cic.term) Hashtbl.t *        (* ids_to_terms *)
-    (Cic.id, Cic.id option) Hashtbl.t *   (* ids_to_father_ids *)
-    (Cic.id, sort_kind) Hashtbl.t *       (* ids_to_inner_sorts *)
-    (Cic.id, Cic.hypothesis) Hashtbl.t    (* ids_to_hypotheses *)
+   Cic.conjecture ->                      (* sequent *)
+    Cic.conjecture *                       (* unshared sequent *)
+    (Cic.annconjecture *                   (* annotated sequent *)
+    (Cic.id, Cic.term) Hashtbl.t *         (* ids_to_terms *)
+    (Cic.id, Cic.id option) Hashtbl.t *    (* ids_to_father_ids *)
+    (Cic.id, sort_kind) Hashtbl.t *        (* ids_to_inner_sorts *)
+    (Cic.id, Cic.hypothesis) Hashtbl.t)    (* ids_to_hypotheses *)
 
 val plain_acic_object_of_cic_object : Cic.obj -> Cic.annobj