diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-03-12 13:39:51 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-03-12 13:39:51 +0000 |
| commit | 09ab4a94562c1633cfbabdc6dce959c61cffa90f (patch) | |
| tree | ca40eeff1bb4aa4746885250f865dea6cf48986d /theories7 | |
| parent | b9025b5b986e3243042bde2566490d37209d2c8c (diff) | |
Bug compatibilite
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5465 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories7')
| -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 1249e62ea..6fc763807 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). |