From 039b2423cf7b85f2f5960dde6a1586f0f07cf9d0 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 29 Sep 2019 00:06:19 +0200
Subject: Addressing #6082 and #7766 (overriding format of notation).

We do two changes:
- We distinguish between a notion of format generically attached to
  notations and a new notion of format attached to interpreted
  notations. "Reserved Notation" attaches a format
  generically. "Notation" attaches the format specifically to the given
  interpretation, and additionally, attaches it generically if it is the
  first time the notation is defined.
- We warn before overriding an explicitly reserved generic format, or
  a specific format.
---
 printing/proof_diffs.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'printing/proof_diffs.ml')

diff --git a/printing/proof_diffs.ml b/printing/proof_diffs.ml
index d93dd15f91..c3ee5968dc 100644
--- a/printing/proof_diffs.ml
+++ b/printing/proof_diffs.ml
@@ -529,7 +529,7 @@ let match_goals ot nt =
         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) ->
+    | CNotation (_,ntn,args), CNotation (_,ntn2,args2) ->
       constr_notation_substitution ogname args args2
     | CGeneralization (b,a,c), CGeneralization (b2,a2,c2) ->
       constr_expr ogname c c2
-- 
cgit v1.2.3