X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Focaml%2Fcic_disambiguation%2Flogic_notation.ml;h=1d47711da721d2d9419169d460acf0df76ab9512;hb=e626927b4c1c77bdcd6b545203a0a9c17a9ff136;hp=a19361b32e7264717b96e5f5fc185353d50fff99;hpb=67eafee21527f29a9b26fd1a7c518e0b49c24bf5;p=helm.git

diff --git a/helm/ocaml/cic_disambiguation/logic_notation.ml b/helm/ocaml/cic_disambiguation/logic_notation.ml
index a19361b32..1d47711da 100644
--- a/helm/ocaml/cic_disambiguation/logic_notation.ml
+++ b/helm/ocaml/cic_disambiguation/logic_notation.ml
@@ -57,6 +57,6 @@ let _ =
        in
        Cic.Appl [
          Cic.MutInd (HelmLibraryObjects.Logic.eq_URI, 0, []);
-           Cic.Implicit; t1; t2
+           Cic.Implicit (Some `Type); t1; t2
        ]))