Yet another implementation of the single aliases / multi aliases idea.

[helm.git] / helm / matita / matitaTypes.mli

diff --git a/helm/matita/matitaTypes.mli b/helm/matita/matitaTypes.mli
index c0946c89f8a0c8990d073ff489a3afa8b1be7c32..51744f15296240242f0e5e51747e339dc551069f 100644 (file)
--- a/helm/matita/matitaTypes.mli
+++ b/helm/matita/matitaTypes.mli
@@ -51,6 +51,7 @@ type ast_command = (CicNotationPt.term, GrafiteAst.obj) GrafiteAst.command
 
 type status = {
   aliases: DisambiguateTypes.environment;   (** disambiguation aliases *)
+  multi_aliases: DisambiguateTypes.multiple_environment;
   moo_content_rev: ast_command list;
   proof_status: proof_status;
   options: options;