Merge PR #916: Fixing notation bug 5608 involving { } and a slight restructuration

5 files changed, 12 insertions, 54 deletions

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 54861ae4c..e85415bed 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -320,38 +320,6 @@ let drop_implicits_in_patt cst nb_expl args =
        let imps = List.skipn_at_least nb_expl (select_stronger_impargs impl_st) in
        impls_fit [] (imps,args)
 
-let has_curly_brackets ntn =
-  String.length ntn >= 6 && (String.is_sub "{ _ } " ntn 0 ||
-    String.is_sub " { _ }" ntn (String.length ntn - 6) ||
-    String.string_contains ~where:ntn ~what:" { _ } ")
-
-let rec wildcards ntn n =
-  if Int.equal n (String.length ntn) then []
-  else let l = spaces ntn (n+1) in if ntn.[n] == '_' then n::l else l
-and spaces ntn n =
-  if Int.equal n (String.length ntn) then []
-  else if ntn.[n] == ' ' then wildcards ntn (n+1) else spaces ntn (n+1)
-
-let expand_curly_brackets loc mknot ntn l =
-  let ntn' = ref ntn in
-  let rec expand_ntn i =
-    function
-    | [] -> []
-    | a::l ->
-        let a' =
-          let p = List.nth (wildcards !ntn' 0) i - 2 in
-          if p>=0 && p+5 <= String.length !ntn' && String.is_sub "{ _ }" !ntn' p
-          then begin
-            ntn' :=
-              String.sub !ntn' 0 p ^ "_" ^
-              String.sub !ntn' (p+5) (String.length !ntn' -p-5);
-            mknot (loc,"{ _ }",[a]) end
-          else a in
-        a' :: expand_ntn (i+1) l in
-  let l = expand_ntn 0 l in
-  (* side effect *)
-  mknot (loc,!ntn',l)
-
 let destPrim = function { CAst.v = CPrim t } -> Some t | _ -> None
 let destPatPrim = function { CAst.v = CPatPrim t } -> Some t | _ -> None
 
@@ -367,9 +335,7 @@ let is_zero s =
   in aux 0
 
 let make_notation_gen loc ntn mknot mkprim destprim l =
-  if has_curly_brackets ntn
-  then expand_curly_brackets loc mknot ntn l
-  else match ntn,List.map destprim l with
+  match ntn,List.map destprim l with
     (* Special case to avoid writing "- 3" for e.g. (Z.opp 3) *)
     | "- _", [Some (Numeral (p,true))] when not (is_zero p) ->
         mknot (loc,ntn,([mknot (loc,"( _ )",l)]))
diff --git a/interp/notation.ml b/interp/notation.ml
index c07a00943..c373faf68 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -41,7 +41,6 @@ open Context.Named.Declaration
 (**********************************************************************)
 (* Scope of symbols *)
 
-type level = precedence * tolerability list
 type delimiters = string
 type notation_location = (DirPath.t * DirPath.t) * string
 
@@ -83,11 +82,18 @@ let parenRelation_eq t1 t2 = match t1, t2 with
 | Prec l1, Prec l2 -> Int.equal l1 l2
 | _ -> false
 
-let level_eq (l1, t1) (l2, t2) =
+let notation_var_internalization_type_eq v1 v2 = match v1, v2 with
+| NtnInternTypeConstr, NtnInternTypeConstr -> true
+| NtnInternTypeBinder, NtnInternTypeBinder -> true
+| NtnInternTypeIdent, NtnInternTypeIdent -> true
+| (NtnInternTypeConstr | NtnInternTypeBinder | NtnInternTypeIdent), _ -> false
+
+let level_eq (l1, t1, u1) (l2, t2, u2) =
   let tolerability_eq (i1, r1) (i2, r2) =
     Int.equal i1 i2 && parenRelation_eq r1 r2
   in
   Int.equal l1 l2 && List.equal tolerability_eq t1 t2
+  && List.equal notation_var_internalization_type_eq u1 u2
 
 let declare_scope scope =
   try let _ = String.Map.find scope !scope_map in ()
diff --git a/interp/notation.mli b/interp/notation.mli
index e63ad10cd..f9f247fe1 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -21,7 +21,6 @@ open Ppextend
 (** A scope is a set of interpreters for symbols + optional
    interpreter and printers for integers + optional delimiters *)
 
-type level = precedence * tolerability list
 type delimiters = string
 type scope
 type scopes (** = [scope_name list] *)
diff --git a/interp/ppextend.ml b/interp/ppextend.ml
index 2bbe87bbc..3ebc9b71d 100644
--- a/interp/ppextend.ml
+++ b/interp/ppextend.ml
@@ -7,17 +7,10 @@
 (************************************************************************)
 
 open Pp
+open Notation_term
 
 (*s Pretty-print. *)
 
-(* Dealing with precedences *)
-
-type precedence = int
-
-type parenRelation = L | E | Any | Prec of precedence
-
-type tolerability = precedence * parenRelation
-
 type ppbox =
   | PpHB of int
   | PpHOVB of int
diff --git a/interp/ppextend.mli b/interp/ppextend.mli
index a347a5c7b..6ff5a4272 100644
--- a/interp/ppextend.mli
+++ b/interp/ppextend.mli
@@ -6,15 +6,9 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(** {6 Pretty-print. } *)
-
-(** Dealing with precedences *)
-
-type precedence = int
+open Notation_term
 
-type parenRelation = L | E | Any | Prec of precedence
-
-type tolerability = precedence * parenRelation
+(** {6 Pretty-print. } *)
 
 type ppbox =
   | PpHB of int