diff options
author | 2012-08-20 18:27:02 +0200 | |
---|---|---|
committer | 2012-08-20 18:27:02 +0200 | |
commit | 595aa062e10b8d7100ec2ad9b766f9e624e47295 (patch) | |
tree | 963f9c948173de70209cba5828b372f184afc306 /theories/Init | |
parent | ab08ae9f0f944d9f801c44e4ffd3e6b7fcf4b024 (diff) | |
parent | e0d682ec25282a348d35c5b169abafec48555690 (diff) |
Merge tag 'upstream/8.4dfsg' into experimental/master
Upstream version 8.4dfsg
Diffstat (limited to 'theories/Init')
-rw-r--r-- | theories/Init/Datatypes.v | 24 | ||||
-rw-r--r-- | theories/Init/Logic.v | 24 | ||||
-rw-r--r-- | theories/Init/Logic_Type.v | 12 | ||||
-rw-r--r-- | theories/Init/Notations.v | 2 | ||||
-rw-r--r-- | theories/Init/Peano.v | 26 | ||||
-rw-r--r-- | theories/Init/Prelude.v | 2 | ||||
-rw-r--r-- | theories/Init/Specif.v | 28 | ||||
-rw-r--r-- | theories/Init/Tactics.v | 12 | ||||
-rw-r--r-- | theories/Init/Wf.v | 4 |
9 files changed, 67 insertions, 67 deletions
diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v index 41f6b70b..fc620f71 100644 --- a/theories/Init/Datatypes.v +++ b/theories/Init/Datatypes.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -72,7 +72,7 @@ Hint Resolve andb_prop: bool. Lemma andb_true_intro : forall b1 b2:bool, b1 = true /\ b2 = true -> andb b1 b2 = true. Proof. - destruct b1; destruct b2; simpl in |- *; tauto || auto with bool. + destruct b1; destruct b2; simpl; intros [? ?]; assumption. Qed. Hint Resolve andb_true_intro: bool. @@ -203,7 +203,7 @@ Lemma injective_projections : forall (A B:Type) (p1 p2:A * B), fst p1 = fst p2 -> snd p1 = snd p2 -> p1 = p2. Proof. - destruct p1; destruct p2; simpl in |- *; intros Hfst Hsnd. + destruct p1; destruct p2; simpl; intros Hfst Hsnd. rewrite Hfst; rewrite Hsnd; reflexivity. Qed. @@ -344,14 +344,14 @@ Definition id : ID := fun A x => x. (* Compatibility *) -Notation prodT := prod (only parsing). -Notation pairT := pair (only parsing). -Notation prodT_rect := prod_rect (only parsing). -Notation prodT_rec := prod_rec (only parsing). -Notation prodT_ind := prod_ind (only parsing). -Notation fstT := fst (only parsing). -Notation sndT := snd (only parsing). -Notation prodT_uncurry := prod_uncurry (only parsing). -Notation prodT_curry := prod_curry (only parsing). +Notation prodT := prod (compat "8.2"). +Notation pairT := pair (compat "8.2"). +Notation prodT_rect := prod_rect (compat "8.2"). +Notation prodT_rec := prod_rec (compat "8.2"). +Notation prodT_ind := prod_ind (compat "8.2"). +Notation fstT := fst (compat "8.2"). +Notation sndT := snd (compat "8.2"). +Notation prodT_uncurry := prod_uncurry (compat "8.2"). +Notation prodT_curry := prod_curry (compat "8.2"). (* end hide *) diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v index 9cd0b31b..4e6df444 100644 --- a/theories/Init/Logic.v +++ b/theories/Init/Logic.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -240,12 +240,12 @@ Section universal_quantification. Theorem inst : forall x:A, all (fun x => P x) -> P x. Proof. - unfold all in |- *; auto. + unfold all; auto. Qed. Theorem gen : forall (B:Prop) (f:forall y:A, B -> P y), B -> all P. Proof. - red in |- *; auto. + red; auto. Qed. End universal_quantification. @@ -284,7 +284,7 @@ Section Logic_lemmas. Theorem absurd : forall A C:Prop, A -> ~ A -> C. Proof. - unfold not in |- *; intros A C h1 h2. + unfold not; intros A C h1 h2. destruct (h2 h1). Qed. @@ -313,7 +313,7 @@ Section Logic_lemmas. Theorem not_eq_sym : x <> y -> y <> x. Proof. - red in |- *; intros h1 h2; apply h1; destruct h2; trivial. + red; intros h1 h2; apply h1; destruct h2; trivial. Qed. End equality. @@ -378,14 +378,14 @@ Qed. (* Aliases *) -Notation sym_eq := eq_sym (only parsing). -Notation trans_eq := eq_trans (only parsing). -Notation sym_not_eq := not_eq_sym (only parsing). +Notation sym_eq := eq_sym (compat "8.3"). +Notation trans_eq := eq_trans (compat "8.3"). +Notation sym_not_eq := not_eq_sym (compat "8.3"). -Notation refl_equal := eq_refl (only parsing). -Notation sym_equal := eq_sym (only parsing). -Notation trans_equal := eq_trans (only parsing). -Notation sym_not_equal := not_eq_sym (only parsing). +Notation refl_equal := eq_refl (compat "8.3"). +Notation sym_equal := eq_sym (compat "8.3"). +Notation trans_equal := eq_trans (compat "8.3"). +Notation sym_not_equal := not_eq_sym (compat "8.3"). Hint Immediate eq_sym not_eq_sym: core. diff --git a/theories/Init/Logic_Type.v b/theories/Init/Logic_Type.v index 2a833576..0281c516 100644 --- a/theories/Init/Logic_Type.v +++ b/theories/Init/Logic_Type.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -44,7 +44,7 @@ Section identity_is_a_congruence. Lemma not_identity_sym : notT (identity x y) -> notT (identity y x). Proof. - red in |- *; intros H H'; apply H; destruct H'; trivial. + red; intros H H'; apply H; destruct H'; trivial. Qed. End identity_is_a_congruence. @@ -66,7 +66,7 @@ Defined. Hint Immediate identity_sym not_identity_sym: core v62. -Notation refl_id := identity_refl (only parsing). -Notation sym_id := identity_sym (only parsing). -Notation trans_id := identity_trans (only parsing). -Notation sym_not_id := not_identity_sym (only parsing). +Notation refl_id := identity_refl (compat "8.3"). +Notation sym_id := identity_sym (compat "8.3"). +Notation trans_id := identity_trans (compat "8.3"). +Notation sym_not_id := not_identity_sym (compat "8.3"). diff --git a/theories/Init/Notations.v b/theories/Init/Notations.v index 490cbf57..323dab90 100644 --- a/theories/Init/Notations.v +++ b/theories/Init/Notations.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/theories/Init/Peano.v b/theories/Init/Peano.v index c3716eaa..8c6fba50 100644 --- a/theories/Init/Peano.v +++ b/theories/Init/Peano.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -54,7 +54,7 @@ Hint Immediate eq_add_S: core. Theorem not_eq_S : forall n m:nat, n <> m -> S n <> S m. Proof. - red in |- *; auto. + red; auto. Qed. Hint Resolve not_eq_S: core. @@ -93,7 +93,7 @@ Hint Resolve (f_equal2 (A1:=nat) (A2:=nat)): core. Lemma plus_n_O : forall n:nat, n = n + 0. Proof. - induction n; simpl in |- *; auto. + induction n; simpl; auto. Qed. Hint Resolve plus_n_O: core. @@ -104,7 +104,7 @@ Qed. Lemma plus_n_Sm : forall n m:nat, S (n + m) = n + S m. Proof. - intros n m; induction n; simpl in |- *; auto. + intros n m; induction n; simpl; auto. Qed. Hint Resolve plus_n_Sm: core. @@ -115,8 +115,8 @@ Qed. (** Standard associated names *) -Notation plus_0_r_reverse := plus_n_O (only parsing). -Notation plus_succ_r_reverse := plus_n_Sm (only parsing). +Notation plus_0_r_reverse := plus_n_O (compat "8.2"). +Notation plus_succ_r_reverse := plus_n_Sm (compat "8.2"). (** Multiplication *) @@ -132,22 +132,22 @@ Hint Resolve (f_equal2 mult): core. Lemma mult_n_O : forall n:nat, 0 = n * 0. Proof. - induction n; simpl in |- *; auto. + induction n; simpl; auto. Qed. Hint Resolve mult_n_O: core. Lemma mult_n_Sm : forall n m:nat, n * m + n = n * S m. Proof. - intros; induction n as [| p H]; simpl in |- *; auto. - destruct H; rewrite <- plus_n_Sm; apply (f_equal S). - pattern m at 1 3 in |- *; elim m; simpl in |- *; auto. + intros; induction n as [| p H]; simpl; auto. + destruct H; rewrite <- plus_n_Sm; apply eq_S. + pattern m at 1 3; elim m; simpl; auto. Qed. Hint Resolve mult_n_Sm: core. (** Standard associated names *) -Notation mult_0_r_reverse := mult_n_O (only parsing). -Notation mult_succ_r_reverse := mult_n_Sm (only parsing). +Notation mult_0_r_reverse := mult_n_O (compat "8.2"). +Notation mult_succ_r_reverse := mult_n_Sm (compat "8.2"). (** Truncated subtraction: [m-n] is [0] if [n>=m] *) @@ -219,7 +219,7 @@ Theorem nat_double_ind : (forall n m:nat, R n m -> R (S n) (S m)) -> forall n m:nat, R n m. Proof. induction n; auto. - destruct m as [| n0]; auto. + destruct m; auto. Qed. (** Maximum and minimum : definitions and specifications *) diff --git a/theories/Init/Prelude.v b/theories/Init/Prelude.v index d85f5363..e723cadf 100644 --- a/theories/Init/Prelude.v +++ b/theories/Init/Prelude.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/theories/Init/Specif.v b/theories/Init/Specif.v index 5b7afc99..d1610f0a 100644 --- a/theories/Init/Specif.v +++ b/theories/Init/Specif.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -226,16 +226,16 @@ Hint Resolve exist exist2 existT existT2: core. (* Compatibility *) -Notation sigS := sigT (only parsing). -Notation existS := existT (only parsing). -Notation sigS_rect := sigT_rect (only parsing). -Notation sigS_rec := sigT_rec (only parsing). -Notation sigS_ind := sigT_ind (only parsing). -Notation projS1 := projT1 (only parsing). -Notation projS2 := projT2 (only parsing). - -Notation sigS2 := sigT2 (only parsing). -Notation existS2 := existT2 (only parsing). -Notation sigS2_rect := sigT2_rect (only parsing). -Notation sigS2_rec := sigT2_rec (only parsing). -Notation sigS2_ind := sigT2_ind (only parsing). +Notation sigS := sigT (compat "8.2"). +Notation existS := existT (compat "8.2"). +Notation sigS_rect := sigT_rect (compat "8.2"). +Notation sigS_rec := sigT_rec (compat "8.2"). +Notation sigS_ind := sigT_ind (compat "8.2"). +Notation projS1 := projT1 (compat "8.2"). +Notation projS2 := projT2 (compat "8.2"). + +Notation sigS2 := sigT2 (compat "8.2"). +Notation existS2 := existT2 (compat "8.2"). +Notation sigS2_rect := sigT2_rect (compat "8.2"). +Notation sigS2_rec := sigT2_rec (compat "8.2"). +Notation sigS2_ind := sigT2_ind (compat "8.2"). diff --git a/theories/Init/Tactics.v b/theories/Init/Tactics.v index 4d64b823..23d9d10e 100644 --- a/theories/Init/Tactics.v +++ b/theories/Init/Tactics.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -75,7 +75,7 @@ Ltac false_hyp H G := (* A case with no loss of information. *) -Ltac case_eq x := generalize (refl_equal x); pattern x at -1; case x. +Ltac case_eq x := generalize (eq_refl x); pattern x at -1; case x. (* use either discriminate or injection on a hypothesis *) @@ -84,13 +84,13 @@ Ltac destr_eq H := discriminate H || (try (injection H; clear H; intro H)). (* Similar variants of destruct *) Tactic Notation "destruct_with_eqn" constr(x) := - destruct x as []_eqn. + destruct x eqn:?. Tactic Notation "destruct_with_eqn" ident(n) := - try intros until n; destruct n as []_eqn. + try intros until n; destruct n eqn:?. Tactic Notation "destruct_with_eqn" ":" ident(H) constr(x) := - destruct x as []_eqn:H. + destruct x eqn:H. Tactic Notation "destruct_with_eqn" ":" ident(H) ident(n) := - try intros until n; destruct n as []_eqn:H. + try intros until n; destruct n eqn:H. (** Break every hypothesis of a certain type *) diff --git a/theories/Init/Wf.v b/theories/Init/Wf.v index 2bb7eae9..c9fcb570 100644 --- a/theories/Init/Wf.v +++ b/theories/Init/Wf.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -103,7 +103,7 @@ Section Well_founded. Lemma Fix_eq : forall x:A, Fix x = F (fun (y:A) (p:R y x) => Fix y). Proof. - intro x; unfold Fix in |- *. + intro x; unfold Fix. rewrite <- Fix_F_eq. apply F_ext; intros. apply Fix_F_inv. |