A step towards supporting pattern cast deeplier.

We at least support a cast at the top of patterns in notations.

1 files changed, 1 insertions, 7 deletions

diff --git a/parsing/g_constr.mlg b/parsing/g_constr.mlg
index 9b4b41acd2..68530178f8 100644
--- a/parsing/g_constr.mlg
+++ b/parsing/g_constr.mlg
@@ -443,13 +443,7 @@ GRAMMAR EXTEND Gram
         { List.map (fun (n, b, t) -> CLocalAssum ([n], Generalized (MaxImplicit, b), t)) tc }
       | "`["; tc = LIST1 typeclass_constraint SEP "," ; "]" ->
         { List.map (fun (n, b, t) -> CLocalAssum ([n], Generalized (NonMaxImplicit, b), t)) tc }
-      | "'"; p = pattern LEVEL "0" ->
-        { let (p, ty) =
-            match p.CAst.v with
-            | CPatCast (p, ty) -> (p, Some ty)
-            | _ -> (p, None)
-          in
-          [CLocalPattern (CAst.make ~loc (p, ty))] } ] ]
+      | "'"; p = pattern LEVEL "0" -> { [CLocalPattern p] } ] ]
   ;
   one_open_binder:
     [ [ na = name -> { (pat_of_name na, Explicit) }