aboutsummaryrefslogtreecommitdiff
path: root/theories/Program
diff options
context:
space:
mode:
Diffstat (limited to 'theories/Program')
-rw-r--r--theories/Program/Basics.v2
-rw-r--r--theories/Program/Combinators.v2
-rw-r--r--theories/Program/Equality.v24
-rw-r--r--theories/Program/Program.v2
-rw-r--r--theories/Program/Subset.v5
-rw-r--r--theories/Program/Syntax.v9
-rw-r--r--theories/Program/Tactics.v8
-rw-r--r--theories/Program/Utils.v4
-rw-r--r--theories/Program/Wf.v6
9 files changed, 31 insertions, 31 deletions
diff --git a/theories/Program/Basics.v b/theories/Program/Basics.v
index e5be0ca925..644b9b5a72 100644
--- a/theories/Program/Basics.v
+++ b/theories/Program/Basics.v
@@ -1,7 +1,7 @@
(* -*- coding: utf-8 -*- *)
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/theories/Program/Combinators.v b/theories/Program/Combinators.v
index e246041b69..772018aa0f 100644
--- a/theories/Program/Combinators.v
+++ b/theories/Program/Combinators.v
@@ -1,7 +1,7 @@
(* -*- coding: utf-8 -*- *)
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/theories/Program/Equality.v b/theories/Program/Equality.v
index a9aa30df5f..d6f9bb9df0 100644
--- a/theories/Program/Equality.v
+++ b/theories/Program/Equality.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -8,7 +8,6 @@
(** Tactics related to (dependent) equality and proof irrelevance. *)
-Require Export ProofIrrelevance.
Require Export JMeq.
Require Import Coq.Program.Tactics.
@@ -143,7 +142,7 @@ Ltac pi_eq_proof_hyp p :=
| [ H : X = Y |- _ ] =>
match p with
| H => fail 2
- | _ => rewrite (proof_irrelevance (X = Y) p H)
+ | _ => rewrite (UIP _ X Y p H)
end
| _ => fail " No hypothesis with same type "
end
@@ -166,7 +165,7 @@ Hint Rewrite <- eq_rect_eq : refl_id.
[coerce_* t eq_refl = t]. *)
Lemma JMeq_eq_refl {A} (x : A) : JMeq_eq (@JMeq_refl _ x) = eq_refl.
-Proof. apply proof_irrelevance. Qed.
+Proof. apply UIP. Qed.
Lemma UIP_refl_refl A (x : A) :
Eqdep.EqdepTheory.UIP_refl A x eq_refl = eq_refl.
@@ -238,8 +237,8 @@ Ltac inject_left H :=
Ltac inject_right H :=
progress (inversion H ; subst_right_no_fail ; clear_dups) ; clear H.
-Ltac autoinjections_left := repeat autoinjection ltac:inject_left.
-Ltac autoinjections_right := repeat autoinjection ltac:inject_right.
+Ltac autoinjections_left := repeat autoinjection ltac:(inject_left).
+Ltac autoinjections_right := repeat autoinjection ltac:(inject_right).
Ltac simpl_depind := subst_no_fail ; autoinjections ; try discriminates ;
simpl_JMeq ; simpl_existTs ; simplify_IH_hyps.
@@ -333,7 +332,7 @@ Ltac simplify_one_dep_elim_term c :=
(let hyp := fresh in intros hyp ;
move hyp before y ; revert_until hyp ; generalize dependent y ;
refine (solution_right _ _ _ _)(* ; intros until 0 *))
- | ?f ?x = ?g ?y -> _ => let H := fresh in progress (intros H ; injection H ; clear H)
+ | ?f ?x = ?g ?y -> _ => let H := fresh in progress (intros H ; simple injection H; clear H)
| ?t = ?u -> _ => let hyp := fresh in
intros hyp ; exfalso ; discriminate
| ?x = ?y -> _ => let hyp := fresh in
@@ -426,8 +425,9 @@ Ltac depind id := do_depind ltac:(fun hyp => do_ind hyp) id.
(** A variant where generalized variables should be given by the user. *)
Ltac do_depelim' rev tac H :=
- (try intros until H) ; block_goal ; rev H ;
- (try revert_until H ; block_goal) ; generalize_eqs H ; tac H ; simpl_dep_elim.
+ (try intros until H) ; block_goal ;
+ (try revert_until H ; block_goal) ;
+ generalize_eqs H ; rev H ; tac H ; simpl_dep_elim.
(** Calls [destruct] on the generalized hypothesis, results should be similar to inversion.
By default, we don't try to generalize the hyp by its variable indices. *)
@@ -463,3 +463,9 @@ Tactic Notation "dependent" "induction" ident(H) "generalizing" ne_hyp_list(l) :
Tactic Notation "dependent" "induction" ident(H) "generalizing" ne_hyp_list(l) "using" constr(c) :=
do_depelim' ltac:(fun hyp => revert l) ltac:(fun hyp => induction hyp using c) H.
+
+Tactic Notation "dependent" "induction" ident(H) "in" ne_hyp_list(l) :=
+ do_depelim' ltac:(fun hyp => idtac) ltac:(fun hyp => induction hyp in l) H.
+
+Tactic Notation "dependent" "induction" ident(H) "in" ne_hyp_list(l) "using" constr(c) :=
+ do_depelim' ltac:(fun hyp => idtac) ltac:(fun hyp => induction hyp in l using c) H.
diff --git a/theories/Program/Program.v b/theories/Program/Program.v
index 5af6f4d742..4a6f2786f8 100644
--- a/theories/Program/Program.v
+++ b/theories/Program/Program.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/theories/Program/Subset.v b/theories/Program/Subset.v
index 50b89b5c07..2a3ec926b2 100644
--- a/theories/Program/Subset.v
+++ b/theories/Program/Subset.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -9,6 +9,7 @@
Require Import Coq.Program.Utils.
Require Import Coq.Program.Equality.
+Require Export ProofIrrelevance.
Local Open Scope program_scope.
@@ -82,7 +83,7 @@ Qed.
Definition match_eq (A B : Type) (x : A) (fn : {y : A | y = x} -> B) : B :=
fn (exist _ x eq_refl).
-(* This is what we want to be able to do: replace the originaly matched object by a new,
+(* This is what we want to be able to do: replace the originally matched object by a new,
propositionally equal one. If [fn] works on [x] it should work on any [y | y = x]. *)
Lemma match_eq_rewrite : forall (A B : Type) (x : A) (fn : {y : A | y = x} -> B)
diff --git a/theories/Program/Syntax.v b/theories/Program/Syntax.v
index 67e9a20cc1..2fccf6249e 100644
--- a/theories/Program/Syntax.v
+++ b/theories/Program/Syntax.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -32,10 +32,3 @@ Require List.
Export List.ListNotations.
Require Import Bvector.
-
-(** Treating n-ary exists *)
-
-Tactic Notation "exists" constr(x) := exists x.
-Tactic Notation "exists" constr(x) constr(y) := exists x ; exists y.
-Tactic Notation "exists" constr(x) constr(y) constr(z) := exists x ; exists y ; exists z.
-Tactic Notation "exists" constr(x) constr(y) constr(z) constr(w) := exists x ; exists y ; exists z ; exists w.
diff --git a/theories/Program/Tactics.v b/theories/Program/Tactics.v
index 0cf8d7337b..dfd6b0eae0 100644
--- a/theories/Program/Tactics.v
+++ b/theories/Program/Tactics.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -41,7 +41,7 @@ Ltac do_nat n tac :=
(** Do something on the last hypothesis, or fail *)
Ltac on_last_hyp tac :=
- match goal with [ H : _ |- _ ] => first [ tac H | fail 1 ] end.
+ lazymatch goal with [ H : _ |- _ ] => tac H end.
(** Destructs one pair, without care regarding naming. *)
@@ -252,7 +252,7 @@ Ltac autoinjection tac :=
Ltac inject H := progress (inversion H ; subst*; clear_dups) ; clear H.
-Ltac autoinjections := repeat (clear_dups ; autoinjection ltac:inject).
+Ltac autoinjections := repeat (clear_dups ; autoinjection ltac:(inject)).
(** Destruct an hypothesis by first copying it to avoid dependencies. *)
@@ -264,7 +264,7 @@ Ltac bang :=
match goal with
| |- ?x =>
match x with
- | appcontext [False_rect _ ?p] => elim p
+ | context [False_rect _ ?p] => elim p
end
end.
diff --git a/theories/Program/Utils.v b/theories/Program/Utils.v
index e39128cb81..396c96181d 100644
--- a/theories/Program/Utils.v
+++ b/theories/Program/Utils.v
@@ -1,12 +1,12 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(** Various syntaxic shortands that are useful with [Program]. *)
+(** Various syntactic shorthands that are useful with [Program]. *)
Require Export Coq.Program.Tactics.
diff --git a/theories/Program/Wf.v b/theories/Program/Wf.v
index d89919b0a0..c490ea5166 100644
--- a/theories/Program/Wf.v
+++ b/theories/Program/Wf.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -89,7 +89,7 @@ Section Measure_well_founded.
Lemma measure_wf: well_founded MR.
Proof with auto.
unfold well_founded.
- cut (forall a: M, (fun mm: M => forall a0: T, m a0 = mm -> Acc MR a0) a).
+ cut (forall (a: M) (a0: T), m a0 = a -> Acc MR a0).
intros.
apply (H (m a))...
apply (@well_founded_ind M R wf (fun mm => forall a, m a = mm -> Acc MR a)).
@@ -211,7 +211,7 @@ Ltac fold_sub f :=
match goal with
| [ |- ?T ] =>
match T with
- appcontext C [ @Fix_sub _ _ _ _ _ ?arg ] =>
+ context C [ @Fix_sub _ _ _ _ _ ?arg ] =>
let app := context C [ f arg ] in
change app
end
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-02 13:32:41 +0000