summaryrefslogtreecommitdiff
path: root/theories/Init
diff options
context:
space:
mode:
Diffstat (limited to 'theories/Init')
-rw-r--r--theories/Init/Datatypes.v24
-rw-r--r--theories/Init/Logic.v24
-rw-r--r--theories/Init/Logic_Type.v12
-rw-r--r--theories/Init/Notations.v2
-rw-r--r--theories/Init/Peano.v26
-rw-r--r--theories/Init/Prelude.v2
-rw-r--r--theories/Init/Specif.v28
-rw-r--r--theories/Init/Tactics.v12
-rw-r--r--theories/Init/Wf.v4
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.
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-06 20:31:45 +0000