diff options
| -rwxr-xr-x | theories7/Init/Logic_Type.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/theories7/Init/Logic_Type.v b/theories7/Init/Logic_Type.v index 1249e62eaa..6fc7638076 100755 --- a/theories7/Init/Logic_Type.v +++ b/theories7/Init/Logic_Type.v @@ -268,9 +268,9 @@ Notation sym_idT := sym_id (only parsing). Notation trans_idT := trans_id (only parsing). Notation congr_idT := congr_id (only parsing). Notation sym_not_idT := sym_not_id (only parsing). -Notation identityT_ind_r := identityT_ind_r (only parsing). -Notation identityT_rec_r := identityT_rec_r (only parsing). -Notation identityT_rect_r := identityT_rect_r (only parsing). +Notation identityT_ind_r := identity_ind_r (only parsing). +Notation identityT_rec_r := identity_rec_r (only parsing). +Notation identityT_rect_r := identity_rect_r (only parsing). ]. Inductive prodT [A,B:Type] : Type := pairT : A -> B -> (prodT A B). |