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 ec4b2e9386..07f27efb51 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -240,6 +240,10 @@ let check_is_hole id = function GHole _ -> () | t -> strbrk "In recursive notation with binders, " ++ pr_id id ++ strbrk " is expected to come without type.") +type recursive_pattern_kind = +| RecursiveTerms of bool (* associativity *) +| RecursiveBinders of glob_constr * glob_constr + let compare_recursive_parts found f (iterator,subc) = let diff = ref None in let terminator = ref None in @@ -261,18 +265,16 @@ let compare_recursive_parts found 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 @@ -286,7 +288,7 @@ let compare_recursive_parts found 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 = (pi1 !found, (x,y) :: pi2 !found, pi3 !found) in let iterator = f (if lassoc then subst_glob_vars [y,GVar(Loc.ghost,x)] iterator @@ -294,11 +296,13 @@ let compare_recursive_parts found 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 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 0000000000..d28303b8ab --- /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. |