From eeb142f3c69d2467fbadd7dd1470ac1606b2e5bf Mon Sep 17 00:00:00 2001
From: Jim Fehrle
Date: Sun, 7 Mar 2021 10:15:11 -0800
Subject: Remove the :> type cast

---
 printing/ppconstr.ml    | 3 +--
 printing/proof_diffs.ml | 1 -
 2 files changed, 1 insertion(+), 3 deletions(-)

(limited to 'printing')

diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index 4c410c3170..e08a494c2e 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -673,8 +673,7 @@ let tag_var = tag Tag.variable
                   match b with
                     | CastConv b -> str ":" ++ ws 1 ++ pr mt (LevelLe (-lcast)) b
                     | CastVM b -> str "<:" ++ ws 1 ++ pr mt (LevelLe (-lcast)) b
-                    | CastNative b -> str "<<:" ++ ws 1 ++ pr mt (LevelLe (-lcast)) b
-                    | CastCoerce -> str ":>"),
+                    | CastNative b -> str "<<:" ++ ws 1 ++ pr mt (LevelLe (-lcast)) b),
           lcast
         )
       | CNotation (_,(_,"( _ )"),([t],[],[],[])) ->
diff --git a/printing/proof_diffs.ml b/printing/proof_diffs.ml
index 9bf765717f..9ba64717d9 100644
--- a/printing/proof_diffs.ml
+++ b/printing/proof_diffs.ml
@@ -529,7 +529,6 @@ let match_goals ot nt =
       | CastVM a, CastVM a2
       | CastNative a, CastNative a2 ->
         constr_expr ogname a a2
-      | CastCoerce, CastCoerce -> ()
       | _, _ -> raise (Diff_Failure "Unable to match goals between old and new proof states (4)"))
     | CNotation (_,ntn,args), CNotation (_,ntn2,args2) ->
       constr_notation_substitution ogname args args2
-- 
cgit v1.2.3