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

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

diff --git a/helm/matita/matitaTypes.ml b/helm/matita/matitaTypes.ml
index 4ac480cf1761b5fed5fbcbcac80d313f995185d0..5df68ea86dca84d94d0ff52b4c86c082a9081935 100644 (file)
--- a/helm/matita/matitaTypes.ml
+++ b/helm/matita/matitaTypes.ml
@@ -61,6 +61,7 @@ type ast_command = (CicNotationPt.term, GrafiteAst.obj) GrafiteAst.command
 
 type status = {
   aliases: DisambiguateTypes.environment;
+  multi_aliases: DisambiguateTypes.multiple_environment;
   moo_content_rev: ast_command list;
   proof_status: proof_status;
   options: options;