diff options
author | 2003-10-17 17:01:24 +0000 | |
---|---|---|
committer | 2003-10-17 17:01:24 +0000 | |
commit | 99a336049389c7c7888537a401848a57c1c8ea46 (patch) | |
tree | 8e4a47c8570bf522d2d23178df7961571f25e234 /theories/Init | |
parent | c6bb30decd15e0d6ef46e14d72472e8ce5dbe627 (diff) |
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
Diffstat (limited to 'theories/Init')
-rwxr-xr-x | theories/Init/Datatypes.v | 9 | ||||
-rwxr-xr-x | theories/Init/Logic.v | 9 |
2 files changed, 18 insertions, 0 deletions
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. |