matitaprover

[helm.git] / helm / software / components / grafite_parser / grafiteDisambiguate.ml

diff --git a/helm/software/components/grafite_parser/grafiteDisambiguate.ml b/helm/software/components/grafite_parser/grafiteDisambiguate.ml
index 76e5e6d86f13ae5257cd30e3a1e3081fecdf0eb9..04521361ddbb27215c87964a11cb697b37ca5171 100644 (file)
--- a/helm/software/components/grafite_parser/grafiteDisambiguate.ml
+++ b/helm/software/components/grafite_parser/grafiteDisambiguate.ml
@@ -294,6 +294,7 @@ let disambiguate_command lexicon_status ~baseuri metasenv (text,prefix_len,cmd)=
   | GrafiteAst.Coercion _
   | GrafiteAst.Default _
   | GrafiteAst.Drop _
+  | GrafiteAst.Print _
   | GrafiteAst.Include _
   | GrafiteAst.Qed _
   | GrafiteAst.Set _ as cmd ->