eq fusionne avec eqT et devient par défaut sur Type,

idem pour ex et exT, ex2 et exT2, all et allT


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3812 85f007b7-540e-0410-9357-904b9bb8a0f7

10 files changed, 101 insertions, 52 deletions

diff --git a/CHANGES b/CHANGES
index 61445214c..7741ea4cf 100644
--- a/CHANGES
+++ b/CHANGES
@@ -7,6 +7,10 @@ A revision of the standard library and of concrete syntax of Coq, including
 - renaming of various standard notions from French to English (esp in ZArith)
 - all notions of the standard library are declared with (strict)
   implicit arguments
+- eq merged with eqT: old eq disappear, new eq (written =) is old eqT
+  and new eqT is syntactic sugar for new eq (notation == is an alias
+  for = and is written as it)
+- similarly, ex, ex2 and all are merged with exT, exT2 and allT.
 
 Vernacular commands
 
diff --git a/contrib/ring/Ring_abstract.v b/contrib/ring/Ring_abstract.v
index f2fe16f3a..98b4cb858 100644
--- a/contrib/ring/Ring_abstract.v
+++ b/contrib/ring/Ring_abstract.v
@@ -138,7 +138,8 @@ Hint SR_plus_zero_right2_T := Resolve (SR_plus_zero_right2 T).
 Hint SR_mult_one_right_T := Resolve (SR_mult_one_right T).
 Hint SR_mult_one_right2_T := Resolve (SR_mult_one_right2 T).
 Hint SR_plus_reg_right_T := Resolve (SR_plus_reg_right T).
-Hints Resolve refl_eqT sym_eqT trans_eqT.
+Hints Resolve refl_equal sym_equal trans_equal.
+(*Hints Resolve refl_eqT sym_eqT trans_eqT.*)
 Hints Immediate T.
 
 Remark iacs_aux_ok : (x:A)(s:abstract_sum)
@@ -445,7 +446,8 @@ Hint Th_plus_zero_right2_T := Resolve (Th_plus_zero_right2 T).
 Hint Th_mult_one_right_T := Resolve (Th_mult_one_right T).
 Hint Th_mult_one_right2_T := Resolve (Th_mult_one_right2 T).
 Hint Th_plus_reg_right_T := Resolve (Th_plus_reg_right T).
-Hints Resolve refl_eqT sym_eqT trans_eqT.
+Hints Resolve refl_equal sym_equal trans_equal.
+(*Hints Resolve refl_eqT sym_eqT trans_eqT.*)
 Hints Immediate T.
 
 Lemma isacs_aux_ok : (x:A)(s:signed_sum)
diff --git a/contrib/ring/Ring_normalize.v b/contrib/ring/Ring_normalize.v
index 4e6317ace..c146dcc33 100644
--- a/contrib/ring/Ring_normalize.v
+++ b/contrib/ring/Ring_normalize.v
@@ -366,7 +366,8 @@ Hint SR_plus_zero_right2_T := Resolve (SR_plus_zero_right2 T).
 Hint SR_mult_one_right_T := Resolve (SR_mult_one_right T).
 Hint SR_mult_one_right2_T := Resolve (SR_mult_one_right2 T).
 Hint SR_plus_reg_right_T := Resolve (SR_plus_reg_right T).
-Hints Resolve refl_eqT sym_eqT trans_eqT.
+Hints Resolve refl_equal sym_equal trans_equal.
+(* Hints Resolve refl_eqT sym_eqT trans_eqT. *)
 Hints Immediate T.
 
 Lemma varlist_eq_prop : (x,y:varlist)
@@ -789,7 +790,8 @@ Hint Th_plus_zero_right2_T := Resolve (Th_plus_zero_right2 T).
 Hint Th_mult_one_right_T := Resolve (Th_mult_one_right T).
 Hint Th_mult_one_right2_T := Resolve (Th_mult_one_right2 T).
 Hint Th_plus_reg_right_T := Resolve (Th_plus_reg_right T).
-Hints Resolve refl_eqT sym_eqT trans_eqT.
+Hints Resolve refl_equal sym_equal trans_equal.
+(*Hints Resolve refl_eqT sym_eqT trans_eqT.*)
 Hints Immediate T.
 
 (*** Definitions *)
diff --git a/contrib/ring/Setoid_ring_normalize.v b/contrib/ring/Setoid_ring_normalize.v
index 085ff557d..c34c972f7 100644
--- a/contrib/ring/Setoid_ring_normalize.v
+++ b/contrib/ring/Setoid_ring_normalize.v
@@ -380,7 +380,8 @@ Hint SSR_plus_zero_right2_T := Resolve (SSR_plus_zero_right2 S T).
 Hint SSR_mult_one_right_T := Resolve (SSR_mult_one_right S T).
 Hint SSR_mult_one_right2_T := Resolve (SSR_mult_one_right2 S T).
 Hint SSR_plus_reg_right_T := Resolve (SSR_plus_reg_right S T).
-Hints Resolve refl_eqT sym_eqT trans_eqT.
+Hints Resolve refl_equal sym_equal trans_equal.
+(*Hints Resolve refl_eqT sym_eqT trans_eqT.*)
 Hints Immediate T.
 
 Lemma varlist_eq_prop : (x,y:varlist)
@@ -1036,7 +1037,8 @@ Hint STh_plus_zero_right2_T := Resolve (STh_plus_zero_right2 S T).
 Hint STh_mult_one_right_T := Resolve (STh_mult_one_right S T).
 Hint STh_mult_one_right2_T := Resolve (STh_mult_one_right2 S T).
 Hint STh_plus_reg_right_T := Resolve (STh_plus_reg_right S plus_morph T).
-Hints Resolve refl_eqT sym_eqT trans_eqT.
+Hints Resolve refl_equal sym_equal trans_equal.
+(*Hints Resolve refl_eqT sym_eqT trans_eqT.*)
 Hints Immediate T.
 
 
diff --git a/interp/coqlib.ml b/interp/coqlib.ml
index d06f6ac52..86857a17c 100644
--- a/interp/coqlib.ml
+++ b/interp/coqlib.ml
@@ -40,7 +40,7 @@ let glob_O = ConstructRef path_of_O
 let glob_S = ConstructRef path_of_S
 
 let eq_path = make_path logic_module (id_of_string "eq")
-let eqT_path = make_path logic_type_module (id_of_string "eqT")
+let eqT_path = make_path logic_module (id_of_string "eq")
 
 let glob_eq = IndRef (eq_path,0)
 let glob_eqT = IndRef (eqT_path,0)
@@ -115,10 +115,10 @@ let coq_sumbool  = constant "Specif" "sumbool"
 let build_coq_sumbool () = Lazy.force coq_sumbool
 
 (* Equality on Type *)
-let coq_eqT_eq = constant "Logic_Type" "eqT"
-let coq_eqT_ind = constant "Logic_Type" "eqT_ind"
-let coq_eqT_congr =constant "Logic_Type" "congr_eqT"
-let coq_eqT_sym  = constant "Logic_Type" "sym_eqT"
+let coq_eqT_eq = constant "Logic" "eq"
+let coq_eqT_ind = constant "Logic" "eq_ind"
+let coq_eqT_congr =constant "Logic" "f_equal"
+let coq_eqT_sym  = constant "Logic" "sym_eq"
 
 let build_coq_eqT_data = {
   eq = (fun () -> Lazy.force coq_eqT_eq);
@@ -183,20 +183,20 @@ let build_coq_ex ()   = Lazy.force coq_ex
 
 (****************************************************************************)
 (*                             Patterns                                     *)
-(* This needs to have interp_constrpattern available ...
-let parse_astconstr s =
+(* This needs to have interp_constrpattern available ... 
+
+let parse_constr s =
   try 
     Pcoq.parse_string Pcoq.Constr.constr_eoi s 
   with Stdpp.Exc_located (_ , (Stream.Failure | Stream.Error _)) ->
     error "Syntax error : not a construction"
 
 let parse_pattern s =
-  Constrintern.interp_constrpattern Evd.empty (Global.env()) (parse_astconstr s)
-
+  Constrintern.interp_constrpattern Evd.empty (Global.env()) (parse_constr s)
 let coq_eq_pattern =
   lazy (snd (parse_pattern "(Coq.Init.Logic.eq ?1 ?2 ?3)"))
 let coq_eqT_pattern =
-  lazy (snd (parse_pattern "(Coq.Init.Logic_Type.eqT ?1 ?2 ?3)"))
+  lazy (snd (parse_pattern "(Coq.Init.Logic.eq ?1 ?2 ?3)"))
 let coq_idT_pattern =
   lazy (snd (parse_pattern "(Coq.Init.Logic_Type.identityT ?1 ?2 ?3)"))
 let coq_existS_pattern =
@@ -209,15 +209,15 @@ let coq_imp_False_pattern =
   lazy (snd (parse_pattern "? -> Coq.Init.Logic.False"))
 let coq_imp_False_pattern =
   lazy (snd (parse_pattern "? -> Coq.Init.Logic.False"))
-let coq_eqdec_partial_pattern
+let coq_eqdec_partial_pattern =
   lazy (snd (parse_pattern "(sumbool (eq ?1 ?2 ?3) ?4)"))
-let coq_eqdec_pattern
+let coq_eqdec_pattern =
   lazy (snd (parse_pattern "(x,y:?1){<?1>x=y}+{~(<?1>x=y)}"))
 *)
 
 (* The following is less readable but does not depend on parsing *)
 let coq_eq_ref      = lazy (reference "Logic" "eq")
-let coq_eqT_ref     = lazy (reference "Logic_Type" "eqT")
+let coq_eqT_ref     = lazy (reference "Logic" "eq")
 let coq_idT_ref     = lazy (reference "Logic_Type" "identityT")
 let coq_existS_ref  = lazy (reference "Specif" "existS")
 let coq_existT_ref  = lazy (reference "Specif" "existT")
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 3eee019ba..27fffec56 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -134,7 +134,7 @@ let abstract_replace (eq,sym_eq) (eqt,sym_eqt) c2 c1 unsafe gl =
     let (e,sym) = 
       match kind_of_term (hnf_type_of gl t1) with 
         | Sort (Prop(Pos)) -> (eq,sym_eq)
-        | Sort (Type(_))   -> (eqt,sym_eqt)
+        | Sort (Type(_))   -> (eq,sym_eq)
         | _                  -> error "replace"
     in 
     (tclTHENLAST (elim_type (applist (e, [t1;c1;c2])))
@@ -209,7 +209,7 @@ let find_eq_pattern aritysort sort =
     | Set_Type       ->  build_coq_eq_data.eq ()
     | Type_Type      ->  build_coq_idT_data.eq ()
     | Set_SetorProp  ->  build_coq_eq_data.eq ()
-    | Type_SetorProp ->  build_coq_eqT_data.eq ()
+    | Type_SetorProp ->  build_coq_eq_data.eq ()
 
 (* [find_positions t1 t2]
 
diff --git a/tactics/setoid_replace.ml b/tactics/setoid_replace.ml
index 389943f30..4468fd4d3 100644
--- a/tactics/setoid_replace.ml
+++ b/tactics/setoid_replace.ml
@@ -83,7 +83,7 @@ let coq_fleche = lazy(constant ["Setoid"] "fleche")
 
 (* Coq constants *)
 
-let coqeq = lazy(global_constant ["Logic_Type"] "eqT")
+let coqeq = lazy(global_constant ["Logic"] "eq")
 
 let coqconj = lazy(global_constant ["Logic"] "conj")
 let coqand = lazy(global_constant ["Logic"] "and")
diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v
index 7636204ab..ab78af469 100755
--- a/theories/Init/Logic.v
+++ b/theories/Init/Logic.v
@@ -99,13 +99,13 @@ Section First_order_quantifiers.
       construction [(all A P)], or simply [(All P)], is provided as an 
       abbreviation of [(x:A)(P x)] *) 
 
-  Inductive ex [A:Set;P:A->Prop] : Prop 
+  Inductive ex [A:Type;P:A->Prop] : Prop 
       := ex_intro : (x:A)(P x)->(ex A P).
 
-  Inductive ex2 [A:Set;P,Q:A->Prop] : Prop
+  Inductive ex2 [A:Type;P,Q:A->Prop] : Prop
       := ex_intro2 : (x:A)(P x)->(Q x)->(ex2 A P Q).
 
-  Definition all := [A:Set][P:A->Prop](x:A)(P x). 
+  Definition all := [A:Type][P:A->Prop](x:A)(P x). 
 
 End First_order_quantifiers.
 
@@ -117,7 +117,7 @@ Section Equality.
       The others properties (symmetry, transitivity, replacement of 
       equals) are proved below *)
 
-  Inductive eq [A:Set;x:A] : A->Prop
+  Inductive eq [A:Type;x:A] : A->Prop
          := refl_equal : (eq A x x).
 
 End Equality.
@@ -134,7 +134,7 @@ Section Logic_lemmas.
   Qed.
 
   Section equality.
-    Variable A,B : Set.
+    Variable A,B : Type.
     Variable f   : A->B.
     Variable x,y,z : A.
 
@@ -158,7 +158,7 @@ Section Logic_lemmas.
 
     Theorem sym_not_eq : (not (eq ? x y)) -> (not (eq ? y x)).
     Proof.
-     Red; Intros h1 h2; Apply h1; Elim h2; Trivial.
+     Red; Intros h1 h2; Apply h1; Case h2; Trivial.
     Qed.
 
     Definition sym_equal     := sym_eq.
@@ -168,7 +168,7 @@ Section Logic_lemmas.
   End equality.
 
 (* Is now a primitive principle 
-  Theorem eq_rect: (A:Set)(x:A)(P:A->Type)(P x)->(y:A)(eq ? x y)->(P y).
+  Theorem eq_rect: (A:Type)(x:A)(P:A->Type)(P x)->(y:A)(eq ? x y)->(P y).
   Proof.
    Intros.
    Cut (identity A x y).
@@ -177,33 +177,33 @@ Section Logic_lemmas.
   Qed.
 *)
 
-  Definition eq_ind_r : (A:Set)(x:A)(P:A->Prop)(P x)->(y:A)(eq ? y x)->(P y).
-   Intros A x P H y H0; Case sym_eq with 1:= H0; Trivial.
+  Definition eq_ind_r : (A:Type)(x:A)(P:A->Prop)(P x)->(y:A)(eq ? y x)->(P y).
+   Intros A x P H y H0; Elim sym_eq with 1:= H0; Trivial.
   Defined.
 
-  Definition eq_rec_r : (A:Set)(x:A)(P:A->Set)(P x)->(y:A)(eq ? y x)->(P y).
-    Intros A x P H y H0; Case sym_eq with 1:= H0; Trivial.
+  Definition eq_rec_r : (A:Type)(x:A)(P:A->Set)(P x)->(y:A)(eq ? y x)->(P y).
+    Intros A x P H y H0; Elim sym_eq with 1:= H0; Trivial.
   Defined.
 
-  Definition eq_rect_r : (A:Set)(x:A)(P:A->Type)(P x)->(y:A)(eq ? y x)->(P y).
+  Definition eq_rect_r : (A:Type)(x:A)(P:A->Type)(P x)->(y:A)(eq ? y x)->(P y).
     Intros A x P H y H0; Elim sym_eq with 1:= H0; Trivial.
   Defined.
 End Logic_lemmas.
 
-Theorem f_equal2 : (A1,A2,B:Set)(f:A1->A2->B)(x1,y1:A1)(x2,y2:A2)
+Theorem f_equal2 : (A1,A2,B:Type)(f:A1->A2->B)(x1,y1:A1)(x2,y2:A2)
   (eq ? x1 y1) -> (eq ? x2 y2) -> (eq ? (f x1 x2) (f y1 y2)).
 Proof.
   Induction 1; Induction 1; Trivial.
 Qed.
 
-Theorem f_equal3 : (A1,A2,A3,B:Set)(f:A1->A2->A3->B)(x1,y1:A1)(x2,y2:A2)
+Theorem f_equal3 : (A1,A2,A3,B:Type)(f:A1->A2->A3->B)(x1,y1:A1)(x2,y2:A2)
   (x3,y3:A3)(eq ? x1 y1) -> (eq ? x2 y2) -> (eq ? x3 y3) 
    -> (eq ? (f x1 x2 x3) (f y1 y2 y3)).
 Proof.
   Induction 1; Induction 1; Induction 1; Trivial.
 Qed.
 
-Theorem f_equal4 : (A1,A2,A3,A4,B:Set)(f:A1->A2->A3->A4->B)
+Theorem f_equal4 : (A1,A2,A3,A4,B:Type)(f:A1->A2->A3->A4->B)
   (x1,y1:A1)(x2,y2:A2)(x3,y3:A3)(x4,y4:A4)
   (eq ? x1 y1) -> (eq ? x2 y2) -> (eq ? x3 y3) -> (eq ? x4 y4)
    -> (eq ? (f x1 x2 x3 x4) (f y1 y2 y3 y4)).
@@ -211,7 +211,7 @@ Proof.
   Induction 1; Induction 1; Induction 1; Induction 1; Trivial.
 Qed.
 
-Theorem f_equal5 : (A1,A2,A3,A4,A5,B:Set)(f:A1->A2->A3->A4->A5->B)
+Theorem f_equal5 : (A1,A2,A3,A4,A5,B:Type)(f:A1->A2->A3->A4->A5->B)
   (x1,y1:A1)(x2,y2:A2)(x3,y3:A3)(x4,y4:A4)(x5,y5:A5)
   (eq ? x1 y1) -> (eq ? x2 y2) -> (eq ? x3 y3) -> (eq ? x4 y4) -> (eq ? x5 y5)
     -> (eq ? (f x1 x2 x3 x4 x5) (f y1 y2 y3 y4 y5)).
diff --git a/theories/Init/Logic_Type.v b/theories/Init/Logic_Type.v
index e4982c1f6..de4d2721f 100755
--- a/theories/Init/Logic_Type.v
+++ b/theories/Init/Logic_Type.v
@@ -18,7 +18,11 @@ Require LogicSyntax.
 (** [allT A P], or simply [(ALLT x | P(x))], stands for [(x:A)(P x)]
    when [A] is of type [Type] *)
 
+(*
 Definition allT := [A:Type][P:A->Prop](x:A)(P x). 
+*)
+
+Syntactic Definition allT := all.
 
 Section universal_quantification.
 
@@ -27,7 +31,7 @@ Variable P : A->Prop.
 
 Theorem inst :  (x:A)(allT ? [x](P x))->(P x).
 Proof.
-Unfold allT; Auto.
+Unfold all; Auto.
 Qed.
 
 Theorem gen : (B:Prop)(f:(y:A)B->(P y))B->(allT A P).
@@ -45,12 +49,23 @@ End universal_quantification.
 (** [exT2 A P Q], or simply [(EXT x | P(x) & Q(x))], stands for the
     existential quantification on both [P] and [Q] when [A] is of
     type [Type] *)
-
+(*
 Inductive  exT [A:Type;P:A->Prop] : Prop
     := exT_intro : (x:A)(P x)->(exT A P).
+*)
+
+Syntactic Definition exT := ex.
+Syntactic Definition exT_intro := ex_intro.
+Syntactic Definition exT_ind  := ex_ind.
 
+(*
 Inductive exT2 [A:Type;P,Q:A->Prop] : Prop
     := exT_intro2 : (x:A)(P x)->(Q x)->(exT2 A P Q).
+*)
+
+Syntactic Definition exT2 := ex2.
+Syntactic Definition exT_intro2 := ex_intro2.
+Syntactic Definition exT2_ind  := ex2_ind.
 
 (** Leibniz equality : [A:Type][x,y:A] (P:A->Prop)(P x)->(P y)
 
@@ -58,11 +73,20 @@ Inductive exT2 [A:Type;P,Q:A->Prop] : Prop
    type [Type]. This equality satisfies reflexivity (by definition), 
    symmetry, transitivity and stability by congruence *)
 
+
+(*
 Inductive eqT [A:Type;x:A] : A -> Prop
                        := refl_eqT : (eqT A x x).
 
-Hints Resolve refl_eqT exT_intro2 exT_intro : core v62.
+Hints Resolve refl_eqT (* exT_intro2 exT_intro *) : core v62.
+*)
+Syntactic Definition eqT      := eq.
+Syntactic Definition refl_eqT := refl_equal.
+Syntactic Definition eqT_ind  := eq_ind.
+Syntactic Definition eqT_rect := eq_rect.
+Syntactic Definition eqT_rec  := eq_rec.
 
+(*
 Section Equality_is_a_congruence.
 
  Variables A,B : Type.
@@ -91,11 +115,19 @@ Section Equality_is_a_congruence.
  Qed.
 
 End Equality_is_a_congruence.
+*)
+Syntactic Definition sym_eqT  := sym_eq.
+Syntactic Definition trans_eqT  := trans_eq.
+Syntactic Definition congr_eqT  := f_equal.
+Syntactic Definition sym_not_eqT  := sym_not_eq.
 
+(*
 Hints Immediate sym_eqT sym_not_eqT : core v62.
+*)
 
 (** This states the replacement of equals by equals *)
 
+(*
 Definition eqT_ind_r : (A:Type)(x:A)(P:A->Prop)(P x)->(y:A)(eqT ? y x)->(P y).
 Intros A x P H y H0; Case sym_eqT with 1:=H0; Trivial.
 Defined.
@@ -107,6 +139,11 @@ Defined.
 Definition eqT_rect_r : (A:Type)(x:A)(P:A->Type)(P x)->(y:A)(eqT ? y x)->(P y).
 Intros A x P H y H0; Case sym_eqT with 1:=H0; Trivial.
 Defined.
+*)
+
+Syntactic Definition eqT_ind_r  := eq_ind_r.
+Syntactic Definition eqT_rec_r  := eq_rec_r.
+Syntactic Definition eqT_rect_r  := eq_rect_r.
 
 (** Some datatypes at the [Type] level *)
 
diff --git a/theories/Init/Logic_TypeSyntax.v b/theories/Init/Logic_TypeSyntax.v
index 1de550267..9cebfb7df 100644
--- a/theories/Init/Logic_TypeSyntax.v
+++ b/theories/Init/Logic_TypeSyntax.v
@@ -12,35 +12,37 @@ Require Logic_Type.
 
 (** Symbolic notations for things in [Logic_type.v] *)
 
-Notation "x == y"  := (eqT ? x y)       (at level 5, no associativity).
+Notation "x == y"  := (eq ? x y) (at level 5, no associativity, only parsing).
 Notation "x === y" := (identityT ? x y) (at level 5, no associativity).
 
+Notation "'eqT'" := eq (at level 0).
+
 (* Order is important to give printing priority to fully typed ALL and EX *)
 
-Notation AllT := (allT ?).
-Notation "'ALLT' x | p"     := (allT ? [x]p)   (at level 10, p at level 8)
+Notation AllT := (all ?).
+Notation "'ALLT' x | p"     := (all ? [x]p)   (at level 10, p at level 8)
   V8only (at level 200, x at level 80).
-Notation "'ALLT' x : t | p" := (allT t [x:t]p) (at level 10, p at level 8)
+Notation "'ALLT' x : t | p" := (all t [x:t]p) (at level 10, p at level 8)
   V8only (at level 200, x at level 80).
 
-Notation ExT  := (exT ?).
-Notation "'EXT' x | p"      := (exT ? [x]p)    (at level 10, p at level 8)
+Notation ExT  := (ex ?).
+Notation "'EXT' x | p"      := (ex ? [x]p)    (at level 10, p at level 8)
   V8only (at level 200, x at level 80).
-Notation "'EXT' x : t | p"  := (exT t [x:t]p)  (at level 10, p at level 8)
+Notation "'EXT' x : t | p"  := (ex t [x:t]p)  (at level 10, p at level 8)
   V8only (at level 200, x at level 80).
 
-Notation ExT2 := (exT2 ?).
-Notation "'EXT' x | p & q"     := (exT2 ? [x]p [x]q)
+Notation ExT2 := (ex2 ?).
+Notation "'EXT' x | p & q"     := (ex2 ? [x]p [x]q)
   (at level 10, p, q at level 8)
   V8only "'EXT2' x | p & q" (at level 200, x at level 80).
-Notation "'EXT' x : t | p & q" := (exT2 t [x:t]p [x:t]q)
+Notation "'EXT' x : t | p & q" := (ex2 t [x:t]p [x:t]q)
   (at level 10, p, q at level 8)
   V8only "'EXT2' x : t | p & q" (at level 200, x at level 80).
 
 (** Parsing only of things in [Logic_type.v] *)
 
 V7only[
-Notation "< A > x == y"  := (eqT A x y)
+Notation "< A > x == y"  := (eq A x y)
    (A annot, at level 1, x at level 0, only parsing).
 
 Notation "< A > x === y" := (identityT A x y)