From 9ee5808746cbcf6e04c08e6a2e798b6cbb34bb06 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 20 May 2017 21:27:34 +0200
Subject: Fixing a too lax constraint for finding recursive binder part of a
 notation.

This was preventing to work examples such as:

Notation "[ x ; .. ; y ; z ]" := ((x,((fun u => u), .. (y,(fun u =>u,z)) ..))).
---
 interp/notation_ops.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'interp')

diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index 6f91009111..95873ea80d 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -287,7 +287,7 @@ let compare_recursive_parts found f f' (iterator,subc) =
       | Some _ -> false
       end
   | GLambda (Name x,_,t_x,c), GLambda (Name y,_,t_y,term)
-  | GProd (Name x,_,t_x,c), GProd (Name y,_,t_y,term) ->
+  | GProd (Name x,_,t_x,c), GProd (Name y,_,t_y,term) when not (Id.equal x y) ->
       (* We found a binding position where it differs *)
       begin match !diff with
       | None ->
-- 
cgit v1.2.3


From dfdaf4de7870cc828b9887b8619b38f01d7e5493 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 20 May 2017 20:38:02 +0200
Subject: Fixing #5523 (missing support for complex constructions in recursive
 notations).

We get rid of a complex function doing both an incremental comparison
and an effect on names (Notation_ops.compare_glob_constr).

For the effect on names, it was actually already done at the time of
turning glob_constr to notation_constr, so it could be skipped here.

For the comparison, we rely on a new incremental variant of
Glob_ops.glob_eq_constr (thanks to Gaëtan for getting rid of the
artificial recursivity in mk_glob_constr_eq).

Seizing the opportunity to get rid of catch-all clauses in
pattern-matching (as advocated by Maxime). Also make indentation
closer to the one of other functions.
---
 interp/notation_ops.ml | 27 +--------------------------
 1 file changed, 1 insertion(+), 26 deletions(-)

(limited to 'interp')

diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index 95873ea80d..04b7f7f3f1 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -22,31 +22,6 @@ open Notation_term
 (**********************************************************************)
 (* Utilities                                                          *)
 
-let on_true_do b f c = if b then (f c; b) else b
-
-let compare_glob_constr f add t1 t2 = match CAst.(t1.v,t2.v) with
-  | GRef (r1,_), GRef (r2,_) -> eq_gr r1 r2
-  | GVar v1, GVar v2 -> on_true_do (Id.equal v1 v2) add (Name v1)
-  | GApp (f1,l1), GApp (f2,l2) -> f f1 f2 && List.for_all2eq f l1 l2
-  | GLambda (na1,bk1,ty1,c1), GLambda (na2,bk2,ty2,c2)
-    when Name.equal na1 na2 && Constrexpr_ops.binding_kind_eq bk1 bk2 ->
-    on_true_do (f ty1 ty2 && f c1 c2) add na1
-  | GProd (na1,bk1,ty1,c1), GProd (na2,bk2,ty2,c2)
-    when Name.equal na1 na2 && Constrexpr_ops.binding_kind_eq bk1 bk2 ->
-      on_true_do (f ty1 ty2 && f c1 c2) add na1
-  | GHole _, GHole _ -> true
-  | GSort s1, GSort s2 -> Miscops.glob_sort_eq s1 s2
-  | GLetIn (na1,b1,t1,c1), GLetIn (na2,b2,t2,c2) when Name.equal na1 na2 ->
-      on_true_do (f b1 b2 && f c1 c2) add na1
-  | (GCases _ | GRec _
-    | GPatVar _ | GEvar _ | GLetTuple _ | GIf _ | GCast _),_
-  | _,(GCases _ | GRec _
-      | GPatVar _ | GEvar _ | GLetTuple _ | GIf _ | GCast _)
-      -> user_err Pp.(str "Unsupported construction in recursive notations.")
-  | (GRef _ | GVar _ | GApp _ | GLambda _ | GProd _
-    | GHole _ | GSort _ | GLetIn _), _
-      -> false
-
 let rec eq_notation_constr (vars1,vars2 as vars) t1 t2 = match t1, t2 with
 | NRef gr1, NRef gr2 -> eq_gr gr1 gr2
 | NVar id1, NVar id2 -> Int.equal (List.index Id.equal id1 vars1) (List.index Id.equal id2 vars2)
@@ -296,7 +271,7 @@ let compare_recursive_parts found f f' (iterator,subc) =
       | Some _ -> false
       end
   | _ ->
-      compare_glob_constr aux (add_name found) c1 c2 in
+      mk_glob_constr_eq aux c1 c2 in
   if aux iterator subc then
     match !diff with
     | None ->
-- 
cgit v1.2.3