From 99a336049389c7c7888537a401848a57c1c8ea46 Mon Sep 17 00:00:00 2001 From: herbelin Date: Fri, 17 Oct 2003 17:01:24 +0000 Subject: Des implicites plus 'naturels' pour eq_ind, identity_ind and co git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4669 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/Init/Datatypes.v | 9 +++++++++ theories/Init/Logic.v | 9 +++++++++ 2 files changed, 18 insertions(+) (limited to 'theories/Init') diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v index 7f86f0cb9..43c301fb3 100755 --- a/theories/Init/Datatypes.v +++ b/theories/Init/Datatypes.v @@ -46,6 +46,15 @@ Inductive identity [A:Type; a:A] : A->Set := refl_identity: (identity A a a). Hints Resolve refl_identity : core v62. +Implicits identity_ind [1]. +Implicits identity_rec [1]. +Implicits identity_rect [1]. +V7only [ +Implicits identity_ind []. +Implicits identity_rec []. +Implicits identity_rect []. +]. + (** [option A] is the extension of A with a dummy element None *) Inductive option [A:Set] : Set := Some : A -> (option A) | None : (option A). diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v index e32bd4205..683058420 100755 --- a/theories/Init/Logic.v +++ b/theories/Init/Logic.v @@ -186,6 +186,15 @@ Notation "x = y" := (eq ? x y) : type_scope. Notation "x <> y :> T" := ~ (!eq T x y) : type_scope. Notation "x <> y" := ~ x=y : type_scope. +Implicits eq_ind [1]. +Implicits eq_rec [1]. +Implicits eq_rect [1]. +V7only [ +Implicits eq_ind []. +Implicits eq_rec []. +Implicits eq_rect []. +]. + Hints Resolve I conj or_introl or_intror refl_equal : core v62. Hints Resolve ex_intro ex_intro2 : core v62. -- cgit v1.2.3