18 files changed, 350 insertions, 49 deletions
diff --git a/configure.ml b/configure.ml
index da6a6f8cbf..277c3d6439 100644
--- a/configure.ml
+++ b/configure.ml
@@ -1054,7 +1054,7 @@ let do_one_instdir (var,msg,uservalue,selfcontainedlayout,unixlayout,locallayout
           try Some (Sys.getenv "COQ_CONFIGURE_PREFIX")
           with
           | Not_found when !prefs.interactive -> None
-          | Not_found -> Some "_build/default/install"
+          | Not_found -> Some "_build/install/default"
         end
       | p -> p
     in match uservalue, env_prefix with
diff --git a/dev/ci/gitlab.bat b/dev/ci/gitlab.bat
index 31bd65af08..a848c49d75 100755
--- a/dev/ci/gitlab.bat
+++ b/dev/ci/gitlab.bat
@@ -8,23 +8,24 @@ TIME /T
 REM List currently used cygwin and target folders for debugging / maintenance purposes
 
 ECHO "Currently used cygwin folders"
-DIR C:\cygwin*
+DIR C:\ci\cygwin*
 ECHO "Currently used target folders"
-DIR C:\coq*
+DIR C:\ci\coq*
+ECHO "Root folders"
+DIR C:\
 
 if %ARCH% == 32 (
   SET ARCHLONG=i686
-  SET CYGROOT=C:\cygwin
   SET SETUP=setup-x86.exe
 )
 
 if %ARCH% == 64 (
   SET ARCHLONG=x86_64
-  SET CYGROOT=C:\cygwin64
   SET SETUP=setup-x86_64.exe
 )
 
-SET DESTCOQ=C:\coq%ARCH%_inst
+SET CYGROOT=C:\ci\cygwin%ARCH%
+SET DESTCOQ=C:\ci\coq%ARCH%
 
 CALL :MakeUniqueFolder %CYGROOT% CYGROOT
 CALL :MakeUniqueFolder %DESTCOQ% DESTCOQ
@@ -93,9 +94,9 @@ GOTO :EOF
 
 :CleanupFolders
   ECHO "Cleaning %CYGROOT%"
-  DEL /S /F /Q "%CYGROOT%" > NUL
+  RMDIR /S /Q "%CYGROOT%"
   ECHO "Cleaning %DESTCOQ%"
-  DEL /S /F /Q "%DESTCOQ%" > NUL
+  RMDIR /S /Q "%DESTCOQ%"
   GOTO :EOF
 
 :MakeUniqueFolder
diff --git a/doc/sphinx/README.rst b/doc/sphinx/README.rst
index 4ad952bdfb..01240a062c 100644
--- a/doc/sphinx/README.rst
+++ b/doc/sphinx/README.rst
@@ -219,6 +219,9 @@ In addition to the objects above, the ``coqrst`` Sphinx plugin defines the follo
           Print nat.
           Definition a := 1.
 
+    The blank line after the directive is required.  If you begin a proof,
+    include an ``Abort`` afterwards to reset coqtop for the next example.
+
     Here is a list of permissible options:
 
     - Display options
diff --git a/doc/sphinx/_static/diffs-coqide-compacted.png b/doc/sphinx/_static/diffs-coqide-compacted.png
new file mode 100644
index 0000000000..b64ffeb269
--- /dev/null
+++ b/doc/sphinx/_static/diffs-coqide-compacted.png
diff --git a/doc/sphinx/_static/diffs-coqide-multigoal.png b/doc/sphinx/_static/diffs-coqide-multigoal.png
new file mode 100644
index 0000000000..4020279267
--- /dev/null
+++ b/doc/sphinx/_static/diffs-coqide-multigoal.png
diff --git a/doc/sphinx/_static/diffs-coqide-on.png b/doc/sphinx/_static/diffs-coqide-on.png
new file mode 100644
index 0000000000..f270397ea3
--- /dev/null
+++ b/doc/sphinx/_static/diffs-coqide-on.png
diff --git a/doc/sphinx/_static/diffs-coqide-removed.png b/doc/sphinx/_static/diffs-coqide-removed.png
new file mode 100644
index 0000000000..8f2e71fdc8
--- /dev/null
+++ b/doc/sphinx/_static/diffs-coqide-removed.png
diff --git a/doc/sphinx/_static/diffs-coqtop-compacted.png b/doc/sphinx/_static/diffs-coqtop-compacted.png
new file mode 100644
index 0000000000..b37f0a6771
--- /dev/null
+++ b/doc/sphinx/_static/diffs-coqtop-compacted.png
diff --git a/doc/sphinx/_static/diffs-coqtop-multigoal.png b/doc/sphinx/_static/diffs-coqtop-multigoal.png
new file mode 100644
index 0000000000..cfedde02ac
--- /dev/null
+++ b/doc/sphinx/_static/diffs-coqtop-multigoal.png
diff --git a/doc/sphinx/_static/diffs-coqtop-on.png b/doc/sphinx/_static/diffs-coqtop-on.png
new file mode 100644
index 0000000000..bdfcf0af1a
--- /dev/null
+++ b/doc/sphinx/_static/diffs-coqtop-on.png
diff --git a/doc/sphinx/_static/diffs-coqtop-on3.png b/doc/sphinx/_static/diffs-coqtop-on3.png
new file mode 100644
index 0000000000..63ff869432
--- /dev/null
+++ b/doc/sphinx/_static/diffs-coqtop-on3.png
diff --git a/doc/sphinx/biblio.bib b/doc/sphinx/biblio.bib
index aa8537c92d..d9eaa2c6c6 100644
--- a/doc/sphinx/biblio.bib
+++ b/doc/sphinx/biblio.bib
@@ -294,6 +294,17 @@ s},
   year        = {1994}
 }
 
+@Article{Myers,
+  author    = {Eugene Myers},
+  title     = {An {O(ND)} difference algorithm and its variations},
+  journal   = {Algorithmica},
+  volume    = {1},
+  number    = {2},
+  year      = {1986},
+  bibsource = {https://link.springer.com/article/10.1007\%2FBF01840446},
+  url       = {http://www.xmailserver.org/diff2.pdf}
+}
+
 @InProceedings{Parent95b,
   author      = {C. Parent},
   booktitle   = {{Mathematics of Program Construction'95}},
diff --git a/doc/sphinx/practical-tools/coq-commands.rst b/doc/sphinx/practical-tools/coq-commands.rst
index 343ca9ed7d..de9e327740 100644
--- a/doc/sphinx/practical-tools/coq-commands.rst
+++ b/doc/sphinx/practical-tools/coq-commands.rst
@@ -85,6 +85,8 @@ Some |Coq| commands call other |Coq| commands. In this case, they look for
 the commands in directory specified by ``$COQBIN``. If this variable is
 not set, they look for the commands in the executable path.
 
+.. _COQ_COLORS:
+
 The ``$COQ_COLORS`` environment variable can be used to specify the set
 of colors used by ``coqtop`` to highlight its output. It uses the same
 syntax as the ``$LS_COLORS`` variable from GNU’s ls, that is, a colon-separated
@@ -93,6 +95,15 @@ list of assignments of the form :n:`name={*; attr}` where
 ANSI escape code. The list of highlight tags can be retrieved with the
 ``-list-tags`` command-line option of ``coqtop``.
 
+The string uses ANSI escape codes to represent attributes.  For example:
+
+        ``export COQ_COLORS=”diff.added=4;48;2;0;0;240:diff.removed=41”``
+
+sets the highlights for added text in diffs to underlined (the 4) with a background RGB
+color (0, 0, 240) and for removed text in diffs to a red background.
+Note that if you specify ``COQ_COLORS``, the predefined attributes are ignored.
+
+
 .. _command-line-options:
 
 By command line options
@@ -164,9 +175,13 @@ and ``coqtop``, unless stated otherwise:
 :-w (all|none|w₁,…,wₙ): Configure the display of warnings. This
   option expects all, none or a comma-separated list of warning names or
   categories (see Section :ref:`controlling-display`).
-:-color (on|off|auto): Enable or not the coloring of output of `coqtop`.
-  Default is auto, meaning that `coqtop` dynamically decides, depending on
-  whether the output channel supports ANSI escape sequences.
+:-color (on|off|auto): *Coqtop only*.  Enable or disable color output.
+  Default is auto, meaning color is shown only if
+  the output channel supports ANSI escape sequences.
+:-diffs (on|off|removed): *Coqtop only*.  Controls highlighting of differences
+  between proof steps.  ``on`` highlights added tokens, ``removed`` highlights both added and
+  removed tokens.  Requires that ``–color`` is enabled.  (see Section
+  :ref:`showing_diffs`).
 :-beautify: Pretty-print each command to *file.beautified* when
   compiling *file.v*, in order to get old-fashioned
   syntax/definitions/notations.
diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst
index 4b1b7719c5..46851050ac 100644
--- a/doc/sphinx/proof-engine/proof-handling.rst
+++ b/doc/sphinx/proof-engine/proof-handling.rst
@@ -495,6 +495,10 @@ Requesting information
             eexists ?[n].
             Show n.
 
+         .. coqtop:: none
+
+            Abort.
+
    .. cmdv:: Show Script
       :name: Show Script
 
@@ -581,6 +585,164 @@ Requesting information
    fixpoint and cofixpoint is violated at some time of the construction
    of the proof without having to wait the completion of the proof.
 
+.. _showing_diffs:
+
+Showing differences between proof steps
+---------------------------------------
+
+
+Coq can automatically highlight the differences between successive proof steps.
+For example, the following screenshots of CoqIDE and coqtop show the application
+of the same :tacn:`intros` tactic.  The tactic creates two new hypotheses, highlighted in green.
+The conclusion is entirely in pale green because although it’s changed, no tokens were added
+to it.  The second screenshot uses the "removed" option, so it shows the conclusion a
+second time with the old text, with deletions marked in red.  Also, since the hypotheses are
+new, no line of old text is shown for them.
+
+.. comment screenshot produced with:
+   Inductive ev : nat -> Prop :=
+   | ev_0 : ev 0
+   | ev_SS : forall n : nat, ev n -> ev (S (S n)).
+
+   Fixpoint double (n:nat) :=
+     match n with
+     | O => O
+     | S n' => S (S (double n'))
+     end.
+
+   Goal forall n, ev n -> exists k, n = double k.
+   intros n E.
+
+..
+
+  .. image:: ../_static/diffs-coqide-on.png
+     :alt: |CoqIDE| with Set Diffs on
+
+..
+
+  .. image:: ../_static/diffs-coqide-removed.png
+     :alt: |CoqIDE| with Set Diffs removed
+
+..
+
+  .. image:: ../_static/diffs-coqtop-on3.png
+     :alt: coqtop with Set Diffs on
+
+How to enable diffs
+```````````````````
+
+.. opt:: Diffs %( "on" %| "off" %| "removed" %)
+
+  .. This ref doesn't work: :opt:`Set Diffs %( "on" %| "off" %| "removed" %)`
+
+  The “on” option highlights added tokens in green, while the “removed” option
+  additionally reprints items with removed tokens in red.  Unchanged tokens in
+  modified items are shown with pale green or red.  (Colors are user-configurable.)
+
+For coqtop, showing diffs can be enabled when starting coqtop with the
+``-diffs on|off|removed`` command-line option or with the ``Set Diffs``
+command within Coq.  You will need to provide the ``-color on|auto`` command-line option when
+you start coqtop in either case.
+
+Colors for coqtop can be configured by setting the ``COQ_COLORS`` environment
+variable.  See section :ref:`customization-by-environment-variables`.  Diffs
+use the tags ``diff.added``, ``diff.added.bg``, ``diff.removed`` and ``diff.removed.bg``.
+
+In CoqIDE, diffs should be enabled from the ``View`` menu.  Don’t use the ``Set Diffs``
+command in CoqIDE.  You can change the background colors shown for diffs from the
+``Edit | Preferences | Tags`` panel by changing the settings for the ``diff.added``,
+``diff.added.bg``, ``diff.removed`` and ``diff.removed.bg`` tags.  This panel also
+lets you control other attributes of the highlights, such as the foreground
+color, bold, italic, underline and strikeout.
+
+Note: As of this writing (August 2018), Proof General will need minor changes
+to be able to show diffs correctly.  We hope it will support this feature soon.
+See https://github.com/ProofGeneral/PG/issues/381 for the current status.
+
+How diffs are calculated
+````````````````````````
+
+Diffs are calculated as follows:
+
+1. Select the old proof state to compare to, which is the proof state before
+   the last tactic that changed the proof.  Changes that only affect the view
+   of the proof, such as ``all: swap 1 2``, are ignored.
+
+2. For each goal in the new proof state, determine what old goal to compare
+   it to—the one it is derived from or is the same as.  Match the hypotheses by
+   name (order is ignored), handling compacted items specially.
+
+3. For each hypothesis and conclusion (the “items”) in each goal, pass
+   them as strings to the lexer to break them into tokens.  Then apply the
+   Myers diff algorithm :cite:`Myers` on the tokens and add appropriate highlighting.
+
+Notes:
+
+* Aside from the highlights, output for the "on" option should be identical
+  to the undiffed output.
+* Goals completed in the last proof step will not be shown even with the
+  "removed" setting.
+
+.. comment The following screenshots show diffs working with multiple goals and with compacted
+   hypotheses.  In the first one, notice that the goal ``P 1`` is not highlighted at
+   all after the split because it has not changed.
+
+    .. todo: Use this script and remove the screenshots when COQ_COLORS
+      works for coqtop in sphinx
+    .. coqtop:: none
+
+      Set Diffs "on".
+      Parameter P : nat -> Prop.
+      Goal P 1 /\ P 2 /\ P 3.
+
+    .. coqtop:: out
+
+      split.
+
+    .. coqtop:: all
+
+      2: split.
+
+    .. coqtop:: none
+
+      Abort.
+
+  ..
+
+    .. coqtop:: none
+
+      Set Diffs "on".
+      Goal forall n m : nat, n + m = m + n.
+      Set Diffs "on".
+
+    .. coqtop:: out
+
+       intros n.
+
+    .. coqtop:: all
+
+      intros m.
+
+    .. coqtop:: none
+
+      Abort.
+
+This screen shot shows the result of applying a :tacn:`split` tactic that replaces one goal
+with 2 goals.  Notice that the goal ``P 1`` is not highlighted at all after
+the split because it has not changed.
+
+..
+
+  .. image:: ../_static/diffs-coqide-multigoal.png
+     :alt: coqide with Set Diffs on with multiple goals
+
+This is how diffs may appear after applying a :tacn:`intro` tactic that results
+in compacted hypotheses:
+
+..
+
+  .. image:: ../_static/diffs-coqide-compacted.png
+     :alt: coqide with Set Diffs on with compacted hyptotheses
 
 Controlling the effect of proof editing commands
 ------------------------------------------------
diff --git a/doc/tools/coqrst/coqdomain.py b/doc/tools/coqrst/coqdomain.py
index edf4e6ec9d..2c69dcfe08 100644
--- a/doc/tools/coqrst/coqdomain.py
+++ b/doc/tools/coqrst/coqdomain.py
@@ -560,6 +560,9 @@ class CoqtopDirective(Directive):
           Print nat.
           Definition a := 1.
 
+    The blank line after the directive is required.  If you begin a proof,
+    include an ``Abort`` afterwards to reset coqtop for the next example.
+
     Here is a list of permissible options:
 
     - Display options
diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v
index 76c39f275d..8a0265438a 100644
--- a/theories/Init/Datatypes.v
+++ b/theories/Init/Datatypes.v
@@ -177,11 +177,12 @@ Arguments inr {A B} _ , A [B] _.
     the pair [pair A B a b] of [a] and [b] is abbreviated [(a,b)] *)
 
 Inductive prod (A B:Type) : Type :=
-  pair : A -> B -> prod A B.
+  pair : A -> B -> A * B
+
+where "x * y" := (prod x y) : type_scope.
 
 Add Printing Let prod.
 
-Notation "x * y" := (prod x y) : type_scope.
 Notation "( x , y , .. , z )" := (pair .. (pair x y) .. z) : core_scope.
 
 Arguments pair {A B} _ _.
@@ -189,18 +190,14 @@ Arguments pair {A B} _ _.
 Section projections.
   Context {A : Type} {B : Type}.
 
-  Definition fst (p:A * B) := match p with
-				| (x, y) => x
-                              end.
-  Definition snd (p:A * B) := match p with
-				| (x, y) => y
-                              end.
+  Definition fst (p:A * B) := match p with (x, y) => x end.
+  Definition snd (p:A * B) := match p with (x, y) => y end.
 End projections.
 
 Hint Resolve pair inl inr: core.
 
 Lemma surjective_pairing :
-  forall (A B:Type) (p:A * B), p = pair (fst p) (snd p).
+  forall (A B:Type) (p:A * B), p = (fst p, snd p).
 Proof.
   destruct p; reflexivity.
 Qed.
@@ -213,13 +210,19 @@ Proof.
   rewrite Hfst; rewrite Hsnd; reflexivity.
 Qed.
 
-Definition prod_uncurry (A B C:Type) (f:prod A B -> C)
-  (x:A) (y:B) : C := f (pair x y).
+Definition prod_uncurry (A B C:Type) (f:A * B -> C)
+  (x:A) (y:B) : C := f (x,y).
 
 Definition prod_curry (A B C:Type) (f:A -> B -> C)
-  (p:prod A B) : C := match p with
-                       | pair x y => f x y
-                       end.
+  (p:A * B) : C := match p with (x, y) => f x y end.
+
+Import EqNotations.
+
+Lemma rew_pair : forall A (P Q : A->Type) x1 x2 (y1:P x1) (y2:Q x1) (H:x1=x2),
+  (rew H in y1, rew H in y2) = rew [fun x => (P x * Q x)%type] H in (y1,y2).
+Proof.
+  destruct H. reflexivity.
+Defined.
 
 (** Polymorphic lists and some operations *)
 
@@ -254,7 +257,6 @@ Definition app (A : Type) : list A -> list A -> list A :=
    | a :: l1 => a :: app l1 m
   end.
 
-
 Infix "++" := app (right associativity, at level 60) : list_scope.
 
 (* Unset Universe Polymorphism. *)
diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v
index 9d60cf54c3..4ec0049a9c 100644
--- a/theories/Init/Logic.v
+++ b/theories/Init/Logic.v
@@ -406,6 +406,37 @@ End EqNotations.
 
 Import EqNotations.
 
+Section equality_dep.
+  Variable A : Type.
+  Variable B : A -> Type.
+  Variable f : forall x, B x.
+  Variables x y : A.
+
+  Theorem f_equal_dep : forall (H: x = y), rew H in f x = f y.
+  Proof.
+    destruct H; reflexivity.
+  Defined.
+
+End equality_dep.
+
+Section equality_dep2.
+
+  Variable A A' : Type.
+  Variable B : A -> Type.
+  Variable B' : A' -> Type.
+  Variable f : A -> A'.
+  Variable g : forall a:A, B a -> B' (f a).
+  Variables x y : A.
+
+  Lemma f_equal_dep2 : forall {A A' B B'} (f : A -> A') (g : forall a:A, B a -> B' (f a))
+  {x1 x2 : A} {y1 : B x1} {y2 : B x2} (H : x1 = x2),
+  rew H in y1 = y2 -> rew f_equal f H in g x1 y1 = g x2 y2.
+  Proof.
+    destruct H, 1. reflexivity.
+  Defined.
+
+End equality_dep2.
+
 Lemma rew_opp_r : forall A (P:A->Type) (x y:A) (H:x=y) (a:P y), rew H in rew <- H in a = a.
 Proof.
 intros.
@@ -492,6 +523,42 @@ Proof.
   destruct e''; reflexivity.
 Defined.
 
+Theorem rew_map : forall A B (P:B->Type) (f:A->B) x1 x2 (H:x1=x2) (y:P (f x1)),
+  rew [fun x => P (f x)] H in y = rew f_equal f H in y.
+Proof.
+  destruct H; reflexivity.
+Defined.
+
+Theorem eq_trans_map : forall {A B} {x1 x2 x3:A} {y1:B x1} {y2:B x2} {y3:B x3},
+  forall (H1:x1=x2) (H2:x2=x3) (H1': rew H1 in y1 = y2) (H2': rew H2 in y2 = y3),
+  rew eq_trans H1 H2 in y1 = y3.
+Proof.
+  intros. destruct H2. exact (eq_trans H1' H2').
+Defined.
+
+Lemma map_subst : forall {A} {P Q:A->Type} (f : forall x, P x -> Q x) {x y} (H:x=y) (z:P x),
+  rew H in f x z = f y (rew H in z).
+Proof.
+  destruct H. reflexivity.
+Defined.
+
+Lemma map_subst_map : forall {A B} {P:A->Type} {Q:B->Type} (f:A->B) (g : forall x, P x -> Q (f x)),
+  forall {x y} (H:x=y) (z:P x), rew f_equal f H in g x z = g y (rew H in z).
+Proof.
+  destruct H. reflexivity.
+Defined.
+
+Lemma rew_swap : forall A (P:A->Type) x1 x2 (H:x1=x2) (y1:P x1) (y2:P x2), rew H in y1 = y2 -> y1 = rew <- H in y2.
+Proof.
+  destruct H. trivial.
+Defined.
+
+Lemma rew_compose : forall A (P:A->Type) x1 x2 x3 (H1:x1=x2) (H2:x2=x3) (y:P x1),
+  rew H2 in rew H1 in y = rew (eq_trans H1 H2) in y.
+Proof.
+  destruct H2. reflexivity.
+Defined.
+
 (** Extra properties of equality *)
 
 Theorem eq_id_comm_l : forall A (f:A->A) (Hf:forall a, a = f a), forall a, f_equal f (Hf a) = Hf (f a).
diff --git a/theories/Init/Specif.v b/theories/Init/Specif.v
index db8857df64..d6a0fb214f 100644
--- a/theories/Init/Specif.v
+++ b/theories/Init/Specif.v
@@ -154,6 +154,10 @@ Section Projections.
 
 End Projections.
 
+Local Notation "( x ; y )" := (existT _ x y) (at level 0, format "( x ;  '/  ' y )").
+Local Notation "x .1" := (projT1 x) (at level 1, left associativity, format "x .1").
+Local Notation "x .2" := (projT2 x) (at level 1, left associativity, format "x .2").
+
 (** [sigT2] of a predicate can be projected to a [sigT].
 
     This allows [projT1] and [projT2] to be usable with [sigT2].
@@ -231,6 +235,7 @@ Proof.
 Qed.
 
 (** Equality of sigma types *)
+
 Import EqNotations.
 Local Notation "'rew' 'dependent' H 'in' H'"
   := (match H with
@@ -244,18 +249,18 @@ Section sigT.
   Local Unset Implicit Arguments.
   (** Projecting an equality of a pair to equality of the first components *)
   Definition projT1_eq {A} {P : A -> Type} {u v : { a : A & P a }} (p : u = v)
-    : projT1 u = projT1 v
-    := f_equal (@projT1 _ _) p.
+    : u.1 = v.1
+    := f_equal (fun x => x.1) p.
 
   (** Projecting an equality of a pair to equality of the second components *)
   Definition projT2_eq {A} {P : A -> Type} {u v : { a : A & P a }} (p : u = v)
-    : rew projT1_eq p in projT2 u = projT2 v
+    : rew projT1_eq p in u.2 = v.2
     := rew dependent p in eq_refl.
 
   (** Equality of [sigT] is itself a [sigT] (forwards-reasoning version) *)
   Definition eq_existT_uncurried {A : Type} {P : A -> Type} {u1 v1 : A} {u2 : P u1} {v2 : P v1}
              (pq : { p : u1 = v1 & rew p in u2 = v2 })
-    : existT _ u1 u2 = existT _ v1 v2.
+    : (u1; u2) = (v1; v2).
   Proof.
     destruct pq as [p q].
     destruct q; simpl in *.
@@ -264,23 +269,55 @@ Section sigT.
 
   (** Equality of [sigT] is itself a [sigT] (backwards-reasoning version) *)
   Definition eq_sigT_uncurried {A : Type} {P : A -> Type} (u v : { a : A & P a })
-             (pq : { p : projT1 u = projT1 v & rew p in projT2 u = projT2 v })
+             (pq : { p : u.1 = v.1 & rew p in u.2 = v.2 })
     : u = v.
   Proof.
     destruct u as [u1 u2], v as [v1 v2]; simpl in *.
     apply eq_existT_uncurried; exact pq.
   Defined.
 
+  Lemma eq_existT_curried {A : Type} {P : A -> Type} {u1 v1 : A} {u2 : P u1} {v2 : P v1}
+             (p : u1 = v1) (q : rew p in u2 = v2) : (u1; u2) = (v1; v2).
+  Proof.
+    destruct p, q. reflexivity.
+  Defined.
+
+  Local Notation "(= u ; v )" := (eq_existT_curried u v) (at level 0, format "(= u ;  '/  ' v )").
+
+  Lemma eq_existT_curried_map {A A' P P'} (f:A -> A') (g:forall u:A, P u -> P' (f u))
+    {u1 v1 : A} {u2 : P u1} {v2 : P v1} (p : u1 = v1) (q : rew p in u2 = v2) :
+    f_equal (fun x => (f x.1; g x.1 x.2)) (= p; q) =
+    (= f_equal f p; f_equal_dep2 f g p q).
+  Proof.
+    destruct p, q. reflexivity.
+  Defined.
+
+  Lemma eq_existT_curried_trans {A P} {u1 v1 w1 : A} {u2 : P u1} {v2 : P v1} {w2 : P w1}
+    (p : u1 = v1) (q : rew p in u2 = v2)
+    (p' : v1 = w1) (q': rew p' in v2 = w2) :
+    eq_trans (= p; q) (= p'; q') =
+      (= eq_trans p p'; eq_trans_map p p' q q').
+  Proof.
+    destruct p', q'. reflexivity.
+  Defined.
+
+  Theorem eq_existT_curried_congr {A P} {u1 v1 : A} {u2 : P u1} {v2 : P v1}
+    {p p' : u1 = v1} {q : rew p in u2 = v2} {q': rew p' in u2 = v2}
+    (r : p = p') : rew [fun H => rew H in u2 = v2] r in q = q' -> (= p; q) = (= p'; q').
+  Proof.
+    destruct r, 1. reflexivity.
+  Qed.
+
   (** Curried version of proving equality of sigma types *)
   Definition eq_sigT {A : Type} {P : A -> Type} (u v : { a : A & P a })
-             (p : projT1 u = projT1 v) (q : rew p in projT2 u = projT2 v)
+             (p : u.1 = v.1) (q : rew p in u.2 = v.2)
     : u = v
     := eq_sigT_uncurried u v (existT _ p q).
 
   (** Equality of [sigT] when the property is an hProp *)
   Definition eq_sigT_hprop {A P} (P_hprop : forall (x : A) (p q : P x), p = q)
              (u v : { a : A & P a })
-             (p : projT1 u = projT1 v)
+             (p : u.1 = v.1)
     : u = v
     := eq_sigT u v p (P_hprop _ _ _).
 
@@ -289,7 +326,7 @@ Section sigT.
       but for simplicity, we don't. *)
   Definition eq_sigT_uncurried_iff {A P}
              (u v : { a : A & P a })
-    : u = v <-> { p : projT1 u = projT1 v & rew p in projT2 u = projT2 v }.
+    : u = v <-> { p : u.1 = v.1 & rew p in u.2 = v.2 }.
   Proof.
     split; [ intro; subst; exists eq_refl; reflexivity | apply eq_sigT_uncurried ].
   Defined.
@@ -305,12 +342,12 @@ Section sigT.
   (** Equivalence of equality of [sigT] involving hProps with equality of the first components *)
   Definition eq_sigT_hprop_iff {A P} (P_hprop : forall (x : A) (p q : P x), p = q)
              (u v : { a : A & P a })
-    : u = v <-> (projT1 u = projT1 v)
+    : u = v <-> (u.1 = v.1)
     := conj (fun p => f_equal (@projT1 _ _) p) (eq_sigT_hprop P_hprop u v).
 
   (** Non-dependent classification of equality of [sigT] *)
   Definition eq_sigT_nondep {A B : Type} (u v : { a : A & B })
-             (p : projT1 u = projT1 v) (q : projT2 u = projT2 v)
+             (p : u.1 = v.1) (q : u.2 = v.2)
     : u = v
     := @eq_sigT _ _ u v p (eq_trans (rew_const _ _) q).
 
@@ -319,8 +356,8 @@ Section sigT.
     : rew [fun a => { p : P a & Q a p }] H in u
       = existT
           (Q y)
-          (rew H in projT1 u)
-          (rew dependent H in (projT2 u)).
+          (rew H in u.1)
+          (rew dependent H in (u.2)).
   Proof.
     destruct H, u; reflexivity.
   Defined.
@@ -416,12 +453,12 @@ Section sigT2.
     : u = v :> { a : A & P a }
     := f_equal _ p.
   Definition projT1_of_sigT2_eq {A} {P Q : A -> Type} {u v : { a : A & P a & Q a }} (p : u = v)
-    : projT1 u = projT1 v
+    : u.1 = v.1
     := projT1_eq (sigT_of_sigT2_eq p).
 
   (** Projecting an equality of a pair to equality of the second components *)
   Definition projT2_of_sigT2_eq {A} {P Q : A -> Type} {u v : { a : A & P a & Q a }} (p : u = v)
-    : rew projT1_of_sigT2_eq p in projT2 u = projT2 v
+    : rew projT1_of_sigT2_eq p in u.2 = v.2
     := rew dependent p in eq_refl.
 
   (** Projecting an equality of a pair to equality of the third components *)
@@ -443,8 +480,8 @@ Section sigT2.
 
   (** Equality of [sigT2] is itself a [sigT2] (backwards-reasoning version) *)
   Definition eq_sigT2_uncurried {A : Type} {P Q : A -> Type} (u v : { a : A & P a & Q a })
-             (pqr : { p : projT1 u = projT1 v
-                    & rew p in projT2 u = projT2 v & rew p in projT3 u = projT3 v })
+             (pqr : { p : u.1 = v.1
+                    & rew p in u.2 = v.2 & rew p in projT3 u = projT3 v })
     : u = v.
   Proof.
     destruct u as [u1 u2 u3], v as [v1 v2 v3]; simpl in *.
@@ -453,8 +490,8 @@ Section sigT2.
 
   (** Curried version of proving equality of sigma types *)
   Definition eq_sigT2 {A : Type} {P Q : A -> Type} (u v : { a : A & P a & Q a })
-             (p : projT1 u = projT1 v)
-             (q : rew p in projT2 u = projT2 v)
+             (p : u.1 = v.1)
+             (q : rew p in u.2 = v.2)
              (r : rew p in projT3 u = projT3 v)
     : u = v
     := eq_sigT2_uncurried u v (existT2 _ _ p q r).
@@ -472,8 +509,8 @@ Section sigT2.
   Definition eq_sigT2_uncurried_iff {A P Q}
              (u v : { a : A & P a & Q a })
     : u = v
-      <-> { p : projT1 u = projT1 v
-          & rew p in projT2 u = projT2 v & rew p in projT3 u = projT3 v }.
+      <-> { p : u.1 = v.1
+          & rew p in u.2 = v.2 & rew p in projT3 u = projT3 v }.
   Proof.
     split; [ intro; subst; exists eq_refl; reflexivity | apply eq_sigT2_uncurried ].
   Defined.
@@ -498,7 +535,7 @@ Section sigT2.
 
   (** Non-dependent classification of equality of [sigT] *)
   Definition eq_sigT2_nondep {A B C : Type} (u v : { a : A & B & C })
-             (p : projT1 u = projT1 v) (q : projT2 u = projT2 v) (r : projT3 u = projT3 v)
+             (p : u.1 = v.1) (q : u.2 = v.2) (r : projT3 u = projT3 v)
     : u = v
     := @eq_sigT2 _ _ _ u v p (eq_trans (rew_const _ _) q) (eq_trans (rew_const _ _) r).
 
@@ -510,8 +547,8 @@ Section sigT2.
       = existT2
           (Q y)
           (R y)
-          (rew H in projT1 u)
-          (rew dependent H in projT2 u)
+          (rew H in u.1)
+          (rew dependent H in u.2)
           (rew dependent H in projT3 u).
   Proof.
     destruct H, u; reflexivity.