+let default_pattern = "",0,(None,[],Some NotationPt.UserInput);;
+let prod_pattern =
+ "",0,(None,[],Some NotationPt.Binder
+ (`Pi, (mk_id "_",Some (NotationPt.Appl
+ [ NotationPt.Implicit `JustOne
+ ; NotationPt.Implicit `JustOne
+ ; NotationPt.UserInput
+ ; NotationPt.Implicit `JustOne ])),
+ NotationPt.Implicit `JustOne));;
+
+let prod_pattern_jm =
+ "",0,(None,[],Some NotationPt.Binder
+ (`Pi, (mk_id "_",Some (NotationPt.Appl
+ [ NotationPt.Implicit `JustOne
+ ; NotationPt.Implicit `JustOne
+ ; NotationPt.UserInput
+ ; NotationPt.Implicit `JustOne
+ ; NotationPt.Implicit `JustOne ])),
+ NotationPt.Implicit `JustOne));;
+
+let hp_pattern n =
+ "",0,(None,[n, NotationPt.Appl
+ [ NotationPt.Implicit `JustOne
+ ; NotationPt.Implicit `JustOne
+ ; NotationPt.UserInput
+ ; NotationPt.Implicit `JustOne ] ],
+ None);;
+
+let hp_pattern_jm n =
+ "",0,(None,[n, NotationPt.Appl
+ [ NotationPt.Implicit `JustOne
+ ; NotationPt.Implicit `JustOne
+ ; NotationPt.UserInput
+ ; NotationPt.Implicit `JustOne
+ ; NotationPt.Implicit `JustOne ] ],
+ None);;