From 23924afa0e4d7ed9ca58fbf5f69dc57685d593fa Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 24 Oct 2020 13:18:09 +0200
Subject: A step towards supporting pattern cast deeplier.

We at least support a cast at the top of patterns in notations.
---
 parsing/g_constr.mlg | 8 +-------
 1 file changed, 1 insertion(+), 7 deletions(-)

(limited to 'parsing')

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) }
-- 
cgit v1.2.3