diff options
| -rw-r--r-- | plugins/funind/glob_term_to_relation.ml | 10 | ||||
| -rw-r--r-- | test-suite/output/Notations4.out | 20 | ||||
| -rw-r--r-- | test-suite/output/Notations4.v | 9 |
3 files changed, 33 insertions, 6 deletions
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index 02964d7ba5..ba0a3bbb5c 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -321,12 +321,10 @@ let build_constructors_of_type ind' argl = construct in let argl = - if List.is_empty argl - then - Array.to_list - (Array.init (cst_narg - npar) (fun _ -> mkGHole ()) - ) - else argl + if List.is_empty argl then + List.make cst_narg (mkGHole ()) + else + List.make npar (mkGHole ()) @ argl in let pat_as_term = mkGApp(mkGRef (ConstructRef(ind',i+1)),argl) diff --git a/test-suite/output/Notations4.out b/test-suite/output/Notations4.out index efa895d709..5bf4ec7bfb 100644 --- a/test-suite/output/Notations4.out +++ b/test-suite/output/Notations4.out @@ -53,3 +53,23 @@ Notation Cn := Foo.FooCn Expands to: Notation Notations4.J.Mfoo.Foo.Bar.Cn let v := 0%test17 in v : myint63 : myint63 +fun y : nat => # (x, z) |-> y & y + : forall y : nat, + (?T1 * ?T2 -> ?T1 * ?T2 * nat) * (?T * ?T0 -> ?T * ?T0 * nat) +where +?T : [y : nat pat : ?T * ?T0 p0 : ?T * ?T0 p := p0 : ?T * ?T0 + |- Type] (pat, p0, p cannot be used) +?T0 : [y : nat pat : ?T * ?T0 p0 : ?T * ?T0 p := p0 : ?T * ?T0 + |- Type] (pat, p0, p cannot be used) +?T1 : [y : nat pat : ?T1 * ?T2 p0 : ?T1 * ?T2 p := p0 : ?T1 * ?T2 + |- Type] (pat, p0, p cannot be used) +?T2 : [y : nat pat : ?T1 * ?T2 p0 : ?T1 * ?T2 p := p0 : ?T1 * ?T2 + |- Type] (pat, p0, p cannot be used) +fun y : nat => # (x, z) |-> (x + y) & (y + z) + : forall y : nat, + (nat * ?T -> nat * ?T * nat) * (?T0 * nat -> ?T0 * nat * nat) +where +?T : [y : nat pat : nat * ?T p0 : nat * ?T p := p0 : nat * ?T + |- Type] (pat, p0, p cannot be used) +?T0 : [y : nat pat : ?T0 * nat p0 : ?T0 * nat p := p0 : ?T0 * nat + |- Type] (pat, p0, p cannot be used) diff --git a/test-suite/output/Notations4.v b/test-suite/output/Notations4.v index b4c65ce196..b33ad17ed4 100644 --- a/test-suite/output/Notations4.v +++ b/test-suite/output/Notations4.v @@ -210,3 +210,12 @@ Module NumeralNotations. Check let v := 0%test17 in v : myint63. End Test17. End NumeralNotations. + +Module K. + +Notation "# x |-> t & u" := ((fun x => (x,t)),(fun x => (x,u))) + (at level 0, x pattern, t, u at level 39). +Check fun y : nat => # (x,z) |-> y & y. +Check fun y : nat => # (x,z) |-> (x + y) & (y + z). + +End K. |