diff options
| -rw-r--r-- | interp/notation_ops.ml | 16 | ||||
| -rw-r--r-- | test-suite/bugs/closed/5161.v | 27 |
2 files changed, 37 insertions, 6 deletions
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index 7b520c1c1..0c5393cf4 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -248,6 +248,10 @@ let check_is_hole id = function GHole _ -> () | t -> let pair_equal eq1 eq2 (a,b) (a',b') = eq1 a a' && eq2 b b' +type recursive_pattern_kind = +| RecursiveTerms of bool (* associativity *) +| RecursiveBinders of glob_constr * glob_constr + let compare_recursive_parts found f f' (iterator,subc) = let diff = ref None in let terminator = ref None in @@ -269,18 +273,16 @@ let compare_recursive_parts found f f' (iterator,subc) = let x,y = if lassoc then y,x else x,y in begin match !diff with | None -> - let () = diff := Some (x, y, Some lassoc) in + let () = diff := Some (x, y, RecursiveTerms lassoc) in true | 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) -> (* We found a binding position where it differs *) - check_is_hole x t_x; - check_is_hole y t_y; begin match !diff with | None -> - let () = diff := Some (x, y, None) in + let () = diff := Some (x, y, RecursiveBinders (t_x,t_y)) in aux c term | Some _ -> false end @@ -294,7 +296,7 @@ let compare_recursive_parts found f f' (iterator,subc) = (* Here, we would need a loc made of several parts ... *) user_err_loc (subtract_loc loc1 loc2,"", str "Both ends of the recursive pattern are the same.") - | Some (x,y,Some lassoc) -> + | Some (x,y,RecursiveTerms lassoc) -> let newfound,x,y,lassoc = if List.mem_f (pair_equal Id.equal Id.equal) (x,y) (pi2 !found) || List.mem_f (pair_equal Id.equal Id.equal) (x,y) (pi3 !found) @@ -312,11 +314,13 @@ let compare_recursive_parts found f f' (iterator,subc) = (* found have been collected by compare_constr *) found := newfound; NList (x,y,iterator,f (Option.get !terminator),lassoc) - | Some (x,y,None) -> + | Some (x,y,RecursiveBinders (t_x,t_y)) -> let newfound = (pi1 !found, pi2 !found, (x,y) :: pi3 !found) in let iterator = f' (subst_glob_vars [x,GVar(Loc.ghost,y)] iterator) in (* found have been collected by compare_constr *) found := newfound; + check_is_hole x t_x; + check_is_hole y t_y; NBinderList (x,y,iterator,f (Option.get !terminator)) else raise Not_found diff --git a/test-suite/bugs/closed/5161.v b/test-suite/bugs/closed/5161.v new file mode 100644 index 000000000..d28303b8a --- /dev/null +++ b/test-suite/bugs/closed/5161.v @@ -0,0 +1,27 @@ +(* Check that the presence of binders with type annotation do not + prevent the recursive binder part to be found *) + +From Coq Require Import Utf8. + +Delimit Scope C_scope with C. +Global Open Scope C_scope. + +Delimit Scope uPred_scope with I. + +Definition FORALL {T : Type} (f : T → Prop) : Prop := ∀ x, f x. + +Notation "∀ x .. y , P" := + (FORALL (λ x, .. (FORALL (λ y, P)) ..)%I) + (at level 200, x binder, y binder, right associativity) : uPred_scope. +Infix "∧" := and : uPred_scope. + +(* The next command fails with + In recursive notation with binders, Φ is expected to come without type. + I would expect this notation to work fine, since the ∀ does support + type annotation. +*) +Notation "'{{{' P } } } e {{{ x .. y ; pat , Q } } }" := + (∀ Φ : _ → _, + (∀ x, .. (∀ y, Q ∧ Φ pat) .. ))%I + (at level 20, x closed binder, y closed binder, + format "{{{ P } } } e {{{ x .. y ; pat , Q } } }") : uPred_scope. |