X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic_disambiguation%2FcicDisambiguate.ml;h=db305e5d5be35be6263eadca1fba077b1db66418;hb=ddd6560f4e70ec3306d223738a441d5f1dd3eac9;hp=e52db62ddf293312f8707cf8cbde58a40528485f;hpb=7ca0a000878e864c92d94f77900bc2ca0ac143b9;p=helm.git

diff --git a/helm/software/components/cic_disambiguation/cicDisambiguate.ml b/helm/software/components/cic_disambiguation/cicDisambiguate.ml
index e52db62dd..db305e5d5 100644
--- a/helm/software/components/cic_disambiguation/cicDisambiguate.ml
+++ b/helm/software/components/cic_disambiguation/cicDisambiguate.ml
@@ -485,7 +485,7 @@ let interpretate_term ~mk_choice ?(create_dummy_ids=false) ~context ~env ~uri
              CicEnvironment.CircularDependency _ -> 
                raise (DisambiguateTypes.Invalid_choice (lazy (loc,"Circular dependency in the environment")))))
     | CicNotationPt.Implicit `Vector -> assert false
-    | CicNotationPt.Implicit `JustOne -> Cic.Implicit None
+    | CicNotationPt.Implicit (`JustOne | `Tagged _) -> Cic.Implicit None
     | CicNotationPt.UserInput -> Cic.Implicit (Some `Hole)
     | CicNotationPt.Num (num, i) ->
        Disambiguate.resolve ~mk_choice ~env