X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_disambiguation%2FcicTextualParser2.ml;h=7c8261faebc372e2c92772bd1e50f3da3fc1af7f;hb=4649be7680244c896149f9a70dd893353577a4fe;hp=2474191fe4f0c9f866b40e8949f40e504e0fd91f;hpb=57f2f0152b79ad7096b72b7e3e83939d63454a88;p=helm.git

diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
index 2474191fe..7c8261fae 100644
--- a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
+++ b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
@@ -209,6 +209,8 @@ EXTEND
         PAREN "]" ->
           return_term loc
             (CicAst.Case (t, indty_ident, outtyp, patterns))
+      | PAREN "("; t1 = term; SYMBOL ":"; t2 = term; PAREN ")" ->
+          return_term loc (CicAst.Appl [CicAst.Symbol ("cast", 0); t1; t2])
       | PAREN "("; t = term; PAREN ")" -> return_term loc t
       ]
     ];