A parser for aliases implemented (required by the Whelp).

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

diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml
index 24872ffd0c408ceffdb163eb58499baa125946c8..c2db06efaeee6b5a708caecd5735a9eace2a94d9 100644 (file)
--- a/helm/matita/matitaEngine.ml
+++ b/helm/matita/matitaEngine.ml
@@ -598,6 +598,8 @@ let eval_command opts status cmd =
       eval_coercion status coercion
   | GrafiteAst.Alias (loc, spec) -> 
      let aliases =
+      (*CSC: Warning: this code should be factorized with the corresponding
+             code in DisambiguatePp *)
       match spec with
       | GrafiteAst.Ident_alias (id,uri) -> 
          DisambiguateTypes.Environment.add