Added initial support for inversion principles in Matita NG.

[helm.git] / helm / software / components / cic_disambiguation / cicDisambiguate.ml

diff --git a/helm/software/components/cic_disambiguation/cicDisambiguate.ml b/helm/software/components/cic_disambiguation/cicDisambiguate.ml
index e52db62ddf293312f8707cf8cbde58a40528485f..db305e5d5be35be6263eadca1fba077b1db66418 100644 (file)
--- 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