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

2 files changed, 18 insertions, 0 deletions

diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v
index 7f86f0cb99..43c301fb3d 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 e32bd4205b..683058420e 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.