From 09ab4a94562c1633cfbabdc6dce959c61cffa90f Mon Sep 17 00:00:00 2001 From: herbelin Date: Fri, 12 Mar 2004 13:39:51 +0000 Subject: Bug compatibilite git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5465 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories7/Init/Logic_Type.v | 6 +++--- 1 file 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). -- cgit v1.2.3