cicNotation* ==> notation*

[helm.git] / matita / components / ng_disambiguation / disambiguateChoices.ml

diff --git a/matita/components/ng_disambiguation/disambiguateChoices.ml b/matita/components/ng_disambiguation/disambiguateChoices.ml
index 3da5f9baa54d1756dec10e8d0ad87d659c582fe0..6c335ab64aa335d16c4c3df9ddf93561c33b1062 100644 (file)
--- a/matita/components/ng_disambiguation/disambiguateChoices.ml
+++ b/matita/components/ng_disambiguation/disambiguateChoices.ml
@@ -57,7 +57,7 @@ let mk_choice  ~mk_appl ~mk_implicit ~term_of_uri ~term_of_nref (dsc, args, appl
   (fun cic_args ->
     let env',rest =
       let names =
-        List.map (function CicNotationPt.IdentArg (_, name) -> name) args
+        List.map (function NotationPt.IdentArg (_, name) -> name) args
       in
        let rec combine_with_rest l1 l2 =
         match l1,l2 with