Implemented keep_simplified.

[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 8830a600dbaa315497030e0c61c716ab19b1c5b7..9c12d1173c6c9b212e021f52b71e24b1d7ea863b 100644 (file)
--- a/helm/software/components/grafite_parser/grafiteDisambiguate.ml
+++ b/helm/software/components/grafite_parser/grafiteDisambiguate.ml
@@ -78,6 +78,7 @@ let ncic_mk_choice = function
            (NCic.Appl l)::tl -> NCic.Appl (l@tl) | l -> NCic.Appl l)
         ~term_of_uri:(fun uri ->
            fst (OCic2NCic.convert_term uri (CicUtil.term_of_uri uri)))
+        ~term_of_nref:(fun nref -> NCic.Const nref)
        name dsc
   | LexiconAst.Number_alias (_, dsc) -> 
        let desc,f = DisambiguateChoices.lookup_num_by_dsc dsc in
@@ -836,6 +837,7 @@ let disambiguate_command lexicon_status ?baseuri metasenv (text,prefix_len,cmd)=
    | GrafiteAst.Print _
    | GrafiteAst.Qed _
    | GrafiteAst.NQed _
+   | GrafiteAst.NUnivConstraint _
    | GrafiteAst.Set _ as cmd ->
        lexicon_status,metasenv,cmd
    | GrafiteAst.Obj (loc,obj) ->