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.
---
 printing/proof_diffs.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'printing/proof_diffs.ml')

diff --git a/printing/proof_diffs.ml b/printing/proof_diffs.ml
index b2ebc61b4e..9bf765717f 100644
--- a/printing/proof_diffs.ml
+++ b/printing/proof_diffs.ml
@@ -433,7 +433,8 @@ let match_goals ot nt =
         constr_expr ogname c c2;
         constr_expr_opt ogname t t2
       | CLocalPattern p, CLocalPattern p2 ->
-        let (p,ty), (p2,ty2) = p.v,p2.v in
+        let ty = match p.v with CPatCast (_,ty) -> Some ty | _ -> None in
+        let ty2 = match p2.v with CPatCast (_,ty) -> Some ty | _ -> None in
         constr_expr_opt ogname ty ty2
       | _, _ -> raise (Diff_Failure "Unable to match goals between old and new proof states (2)")
     in
-- 
cgit v1.2.3