From a4c7f8bd98be2a200489325ff7c5061cf80ab4f3 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 27 Dec 2016 16:53:30 +0100 Subject: Imported Upstream version 8.6 --- theories/Init/Logic_Type.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'theories/Init/Logic_Type.v') diff --git a/theories/Init/Logic_Type.v b/theories/Init/Logic_Type.v index 4a5f2ad6..4536dfc0 100644 --- a/theories/Init/Logic_Type.v +++ b/theories/Init/Logic_Type.v @@ -64,7 +64,7 @@ Definition identity_rect_r : intros A x P H y H0; case identity_sym with (1 := H0); trivial. Defined. -Hint Immediate identity_sym not_identity_sym: core v62. +Hint Immediate identity_sym not_identity_sym: core. Notation refl_id := identity_refl (compat "8.3"). Notation sym_id := identity_sym (compat "8.3"). -- cgit v1.2.3