From 27d4a636cb7f1fbdbced1980808a9b947405eeb5 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Wed, 7 Oct 2015 23:08:45 +0200
Subject: Remove the "exists" overrides from Program. (Fix bug #4360)

---
 theories/Program/Syntax.v | 7 -------
 1 file changed, 7 deletions(-)

(limited to 'theories/Program')

diff --git a/theories/Program/Syntax.v b/theories/Program/Syntax.v
index 67e9a20cc1..892305b499 100644
--- a/theories/Program/Syntax.v
+++ b/theories/Program/Syntax.v
@@ -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.
-- 
cgit v1.2.3


From caeba655b78a0107c1988e5377cdd11fa91c5ea2 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 7 Nov 2015 22:48:15 +0100
Subject: Experimenting removing strong normalization of the mid-statement in
 tactic cut.

---
 theories/Program/Wf.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'theories/Program')

diff --git a/theories/Program/Wf.v b/theories/Program/Wf.v
index d89919b0a0..6e5919b342 100644
--- a/theories/Program/Wf.v
+++ b/theories/Program/Wf.v
@@ -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)).
-- 
cgit v1.2.3


From df3a49a18c5b01984000df9244ecea9c275b30cd Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Mon, 7 Dec 2015 10:52:14 +0100
Subject: Fix some typos.

---
 theories/Program/Subset.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'theories/Program')

diff --git a/theories/Program/Subset.v b/theories/Program/Subset.v
index 50b89b5c07..ce1f7768dd 100644
--- a/theories/Program/Subset.v
+++ b/theories/Program/Subset.v
@@ -82,7 +82,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)
-- 
cgit v1.2.3


From 86f5c0cbfa64c5d0949365369529c5b607878ef8 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Wed, 20 Jan 2016 17:25:10 +0100
Subject: Update copyright headers.

---
 theories/Program/Basics.v      | 2 +-
 theories/Program/Combinators.v | 2 +-
 theories/Program/Equality.v    | 2 +-
 theories/Program/Program.v     | 2 +-
 theories/Program/Subset.v      | 2 +-
 theories/Program/Syntax.v      | 2 +-
 theories/Program/Tactics.v     | 2 +-
 theories/Program/Utils.v       | 2 +-
 theories/Program/Wf.v          | 2 +-
 9 files changed, 9 insertions(+), 9 deletions(-)

(limited to 'theories/Program')

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 ae6fe7dd0a..27e1ca8444 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        *)
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 ce1f7768dd..c8f37318d1 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        *)
diff --git a/theories/Program/Syntax.v b/theories/Program/Syntax.v
index 892305b499..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        *)
diff --git a/theories/Program/Tactics.v b/theories/Program/Tactics.v
index c1d958b9d3..66ca3e577d 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        *)
diff --git a/theories/Program/Utils.v b/theories/Program/Utils.v
index 65fe87801a..396c96181d 100644
--- a/theories/Program/Utils.v
+++ b/theories/Program/Utils.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/Wf.v b/theories/Program/Wf.v
index d89919b0a0..154200d769 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        *)
-- 
cgit v1.2.3


From d5656a6c28f79d59590d4fde60c5158a649d1b65 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 4 Mar 2016 11:16:03 +0100
Subject: Making parentheses mandatory in tactic scopes.

---
 theories/Program/Equality.v | 4 ++--
 theories/Program/Tactics.v  | 2 +-
 2 files changed, 3 insertions(+), 3 deletions(-)

(limited to 'theories/Program')

diff --git a/theories/Program/Equality.v b/theories/Program/Equality.v
index 27e1ca8444..17f05c5113 100644
--- a/theories/Program/Equality.v
+++ b/theories/Program/Equality.v
@@ -238,8 +238,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.
diff --git a/theories/Program/Tactics.v b/theories/Program/Tactics.v
index 66ca3e577d..7384790dae 100644
--- a/theories/Program/Tactics.v
+++ b/theories/Program/Tactics.v
@@ -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. *)
 
-- 
cgit v1.2.3