From 8d27b12365a1d8b3f1670a055537dd3724583baf Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 30 Aug 2020 08:20:29 +0200
Subject: Notations: reworking the treatment of only-parsing and only-printing
 notations.

The (old) original model for notations was to associated both a
parsing and a printing rule to a notation.

Progressively, it become more and more common to have only parsing
notations or even multiple expressions printed with the same notation.

The new model is to attach to a given scope, string and entry at most
one either only-parsing or mixed-parsing-printing rules + an
arbitrarily many unrelated only-printing rules.

Additionally, we anticipate the ability to selectively
activate/deactivate each of those.

This allows to fix in particular #9682 but also to have
more-to-the-point warnings in case a notation overrides or partially
overrides another one.

Rules for importing are not changed (see forthcoming #12984 though).

We also improve the output of "Print Scopes" so that it adds when a
notation is only-parsing, only-printing, or deactivated, or a
combination of those.

Fixes #4738
Fixes #9682
Fixes part 2 of #12908
Fixes #13112
---
 interp/notation_ops.ml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'interp/notation_ops.ml')

diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index 22531b0016..354809252e 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -27,7 +27,9 @@ open Notation_term
 (* helper for NVar, NVar case in eq_notation_constr *)
 let get_var_ndx id vs = try Some (List.index Id.equal id vs) with Not_found -> None
 
-let rec eq_notation_constr (vars1,vars2 as vars) t1 t2 = match t1, t2 with
+let rec eq_notation_constr (vars1,vars2 as vars) t1 t2 =
+(vars1 == vars2 && t1 == t2) ||
+match t1, t2 with
 | NRef gr1, NRef gr2 -> GlobRef.equal gr1 gr2
 | NVar id1, NVar id2 -> (
    match (get_var_ndx id1 vars1,get_var_ndx id2 vars2) with
-- 
cgit v1.2.3