Merge branch 'master' of https://github.com/coq/coq

18 files changed, 131 insertions, 245 deletions

diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md
index e811c116b6..f0e17909c1 100644
--- a/CONTRIBUTING.md
+++ b/CONTRIBUTING.md
@@ -169,7 +169,7 @@ People are generally happy to help and very reactive.
 
 ["Watching" this repository](https://github.com/coq/coq/subscription)
 can result in a very large number of notifications. We advise that if
-you do, either [confifure your mailbox](https://blog.github.com/2017-07-18-managing-large-numbers-of-github-notifications/#prioritize-the-notifications-you-receive)
+you do, either [configure your mailbox](https://blog.github.com/2017-07-18-managing-large-numbers-of-github-notifications/#prioritize-the-notifications-you-receive)
 to handle incoming notifications efficiently, or you read your
 notifications within a web browser. You can configure how you receive
 notifications in [your GitHub settings](https://github.com/settings/notifications),
diff --git a/CREDITS b/CREDITS
index 9b5c1507f5..4c093c204f 100644
--- a/CREDITS
+++ b/CREDITS
@@ -154,6 +154,7 @@ of the Coq Proof assistant during the indicated time:
   Matthias Puech (INRIA-Bologna, 2008-2011)
   Yann Régis-Gianas (INRIA-PPS then IRIF, 2009-now)
   Clément Renard (INRIA, 2001-2004)
+  Talia Ringer (University of Washington, 2019)
   Claudio Sacerdoti Coen (INRIA, 2004-2005)
   Amokrane Saïbi (INRIA, 1993-1998)
   Vincent Semeria (2018)
@@ -170,7 +171,6 @@ of the Coq Proof assistant during the indicated time:
   Nickolai Zeldovich (MIT 2014-2016)
   Théo Zimmermann (ORCID: https://orcid.org/0000-0002-3580-8806,
                    INRIA-PPS then IRIF, 2015-now)
-  Talia Ringer (UW, 2019)
 
 ***************************************************************************
 INRIA refers to:
diff --git a/dev/v8-syntax/syntax-v8.tex b/dev/v8-syntax/syntax-v8.tex
index dd3908c25f..601d52ddda 100644
--- a/dev/v8-syntax/syntax-v8.tex
+++ b/dev/v8-syntax/syntax-v8.tex
@@ -1167,7 +1167,6 @@ $$
 \nlsep \TERM{Show}~\OPT{\NT{num}}
 \nlsep \TERM{Show}~\TERM{Implicit}~\TERM{Arguments}~\OPT{\NT{num}}
 \nlsep \TERM{Show}~\TERM{Node}
-\nlsep \TERM{Show}~\TERM{Script}
 \nlsep \TERM{Show}~\TERM{Existentials}
 \nlsep \TERM{Show}~\TERM{Tree}
 \nlsep \TERM{Show}~\TERM{Conjecture}
diff --git a/doc/changelog/07-commands-and-options/10277-no-show-script.rst b/doc/changelog/07-commands-and-options/10277-no-show-script.rst
new file mode 100644
index 0000000000..7fdeb632b4
--- /dev/null
+++ b/doc/changelog/07-commands-and-options/10277-no-show-script.rst
@@ -0,0 +1,2 @@
+- Remove ``Show Script`` command (deprecated since 8.10)
+  (`#10277 <https://github.com/coq/coq/pull/10277>`_, by Gaëtan Gilbert).
diff --git a/doc/changelog/12-misc/10019-PG-proof-diffs.rst b/doc/changelog/12-misc/10019-PG-proof-diffs.rst
new file mode 100644
index 0000000000..b2d191be26
--- /dev/null
+++ b/doc/changelog/12-misc/10019-PG-proof-diffs.rst
@@ -0,0 +1,3 @@
+- Proof General can now display Coq-generated diffs between proof steps
+  in color.  (`#10019 <https://github.com/coq/coq/pull/10019>`_ and (in Proof General)
+  `#421 <https://github.com/ProofGeneral/PG/pull/421>`_, by Jim Fehrle).
diff --git a/doc/plugin_tutorial/tuto1/src/g_tuto1.mlg b/doc/plugin_tutorial/tuto1/src/g_tuto1.mlg
index 1d0aca1caf..75251d8e33 100644
--- a/doc/plugin_tutorial/tuto1/src/g_tuto1.mlg
+++ b/doc/plugin_tutorial/tuto1/src/g_tuto1.mlg
@@ -94,9 +94,9 @@ VERNAC COMMAND EXTEND Check1 CLASSIFIED AS QUERY
   { let v = Constrintern.interp_constr (Global.env())
       (Evd.from_env (Global.env())) e in
     let (_, ctx) = v in
-    let evd = Evd.from_ctx ctx in
+    let sigma = Evd.from_ctx ctx in
     Feedback.msg_notice
-    (Printer.pr_econstr_env (Global.env()) evd
+    (Printer.pr_econstr_env (Global.env()) sigma
        (Simple_check.simple_check1 v)) }
 END
 
@@ -104,9 +104,9 @@ VERNAC COMMAND EXTEND Check2 CLASSIFIED AS QUERY
 | [ "Cmd6" constr(e) ] ->
   { let v = Constrintern.interp_constr (Global.env())
       (Evd.from_env (Global.env())) e in
-    let evd, ty = Simple_check.simple_check2 v in
+    let sigma, ty = Simple_check.simple_check2 v in
     Feedback.msg_notice
-      (Printer.pr_econstr_env (Global.env()) evd ty) }
+      (Printer.pr_econstr_env (Global.env()) sigma ty) }
 END
 
 VERNAC COMMAND EXTEND Check1 CLASSIFIED AS QUERY
@@ -114,9 +114,9 @@ VERNAC COMMAND EXTEND Check1 CLASSIFIED AS QUERY
   { let v = Constrintern.interp_constr (Global.env())
       (Evd.from_env (Global.env())) e in
     let (a, ctx) = v in
-    let evd = Evd.from_ctx ctx in
+    let sigma = Evd.from_ctx ctx in
       Feedback.msg_notice
-      (Printer.pr_econstr_env (Global.env()) evd
+      (Printer.pr_econstr_env (Global.env()) sigma
          (Simple_check.simple_check3 v)) }
 END
 
@@ -128,9 +128,9 @@ END
 VERNAC COMMAND EXTEND ExamplePrint CLASSIFIED AS QUERY
 | [ "Cmd8" reference(r) ] ->
   { let env = Global.env() in
-    let evd = Evd.from_env env in
+    let sigma = Evd.from_env env in
     Feedback.msg_notice
-    (Printer.pr_econstr_env env evd
+    (Printer.pr_econstr_env env sigma
       (EConstr.of_constr
         (Simple_print.simple_body_access (Nametab.global r)))) }
 END
diff --git a/doc/plugin_tutorial/tuto1/src/simple_check.ml b/doc/plugin_tutorial/tuto1/src/simple_check.ml
index 2949adde73..c2f09c64e0 100644
--- a/doc/plugin_tutorial/tuto1/src/simple_check.ml
+++ b/doc/plugin_tutorial/tuto1/src/simple_check.ml
@@ -1,32 +1,32 @@
 let simple_check1 value_with_constraints =
   begin
     let evalue, st = value_with_constraints in
-    let evd = Evd.from_ctx st in
+    let sigma = Evd.from_ctx st in
 (* This is reverse engineered from vernacentries.ml *)
 (* The point of renaming is to make sure the bound names printed by Check
    can be re-used in `apply with` tactics that use bound names to
    refer to arguments. *)
     let j = Environ.on_judgment EConstr.of_constr
       (Arguments_renaming.rename_typing (Global.env())
-         (EConstr.to_constr evd evalue)) in
+         (EConstr.to_constr sigma evalue)) in
     let {Environ.uj_type=x}=j in x
   end
 
 let simple_check2 value_with_constraints =
   let evalue, st = value_with_constraints in
-  let evd = Evd.from_ctx st in
+  let sigma = Evd.from_ctx st in
 (* This version should be preferred if bound variable names are not so
   important, you want to really verify that the input is well-typed,
   and if you want to obtain the type. *)
 (* Note that the output value is a pair containing a new evar_map:
    typing will fill out blanks in the term by add evar bindings. *)
-  Typing.type_of (Global.env()) evd evalue
+  Typing.type_of (Global.env()) sigma evalue
 
 let simple_check3 value_with_constraints =
   let evalue, st = value_with_constraints in
-  let evd = Evd.from_ctx st in
+  let sigma = Evd.from_ctx st in
 (* This version should be preferred if bound variable names are not so
   important and you already expect the input to have been type-checked
   before.  Set ~lax to false if you want an anomaly to be raised in
   case of a type error.  Otherwise a ReTypeError exception is raised. *)
-  Retyping.get_type_of ~lax:true (Global.env()) evd evalue
+  Retyping.get_type_of ~lax:true (Global.env()) sigma evalue
diff --git a/doc/plugin_tutorial/tuto3/src/construction_game.ml b/doc/plugin_tutorial/tuto3/src/construction_game.ml
index 663113d012..2a2acb6001 100644
--- a/doc/plugin_tutorial/tuto3/src/construction_game.ml
+++ b/doc/plugin_tutorial/tuto3/src/construction_game.ml
@@ -3,15 +3,15 @@ open Context
 
 let find_reference = Coqlib.find_reference [@ocaml.warning "-3"]
 
-let example_sort evd =
+let example_sort sigma =
 (* creating a new sort requires that universes should be recorded
   in the evd datastructure, so this datastructure also needs to be
   passed around. *)
-  let evd, s = Evd.new_sort_variable Evd.univ_rigid evd in
+  let sigma, s = Evd.new_sort_variable Evd.univ_rigid sigma in
   let new_type = EConstr.mkSort s in
-  evd, new_type
+  sigma, new_type
 
-let c_one evd =
+let c_one sigma =
 (* In the general case, global references may refer to universe polymorphic
    objects, and their universe has to be made afresh when creating an instance. *)
   let gr_S =
@@ -19,129 +19,129 @@ let c_one evd =
 (* the long name of "S" was found with the command "About S." *)
   let gr_O =
     find_reference "Tuto3" ["Coq"; "Init"; "Datatypes"] "O" in
-  let evd, c_O = Evarutil.new_global evd gr_O in
-  let evd, c_S = Evarutil.new_global evd gr_S in
+  let sigma, c_O = Evarutil.new_global sigma gr_O in
+  let sigma, c_S = Evarutil.new_global sigma gr_S in
 (* Here is the construction of a new term by applying functions to argument. *)
-  evd, EConstr.mkApp (c_S, [| c_O |])
+  sigma, EConstr.mkApp (c_S, [| c_O |])
 
-let dangling_identity env evd =
+let dangling_identity env sigma =
 (* I call this a dangling identity, because it is not polymorph, but
    the type on which it applies is left unspecified, as it is
    represented by an existential variable.  The declaration for this
    existential variable needs to be added in the evd datastructure. *)
-  let evd, type_type = example_sort evd in
-  let evd, arg_type = Evarutil.new_evar env evd type_type in
+  let sigma, type_type = example_sort sigma in
+  let sigma, arg_type = Evarutil.new_evar env sigma type_type in
 (* Notice the use of a De Bruijn index for the inner occurrence of the
   bound variable. *)
-  evd, EConstr.mkLambda(nameR (Names.Id.of_string "x"), arg_type,
+  sigma, EConstr.mkLambda(nameR (Names.Id.of_string "x"), arg_type,
           EConstr.mkRel 1)
 
-let dangling_identity2 env evd =
+let dangling_identity2 env sigma =
 (* This example uses directly a function that produces an evar that
   is meant to be a type. *)
-  let evd, (arg_type, type_type) =
-    Evarutil.new_type_evar env evd Evd.univ_rigid in
-  evd, EConstr.mkLambda(nameR (Names.Id.of_string "x"), arg_type,
+  let sigma, (arg_type, type_type) =
+    Evarutil.new_type_evar env sigma Evd.univ_rigid in
+  sigma, EConstr.mkLambda(nameR (Names.Id.of_string "x"), arg_type,
           EConstr.mkRel 1)
 
 let example_sort_app_lambda () =
     let env = Global.env () in
-    let evd = Evd.from_env env in
-    let evd, c_v = c_one evd in
+    let sigma = Evd.from_env env in
+    let sigma, c_v = c_one sigma in
 (* dangling_identity and dangling_identity2 can be used interchangeably here *)
-    let evd, c_f = dangling_identity2 env evd in
+    let sigma, c_f = dangling_identity2 env sigma in
     let c_1 = EConstr.mkApp (c_f, [| c_v |]) in
     let _ = Feedback.msg_notice
-       (Printer.pr_econstr_env env evd c_1) in
+       (Printer.pr_econstr_env env sigma c_1) in
     (* type verification happens here.  Type verification will update
        existential variable information in the evd part. *)
-    let evd, the_type = Typing.type_of env evd c_1 in
+    let sigma, the_type = Typing.type_of env sigma c_1 in
 (* At display time, you will notice that the system knows about the
   existential variable being instantiated to the "nat" type, even
   though c_1 still contains the meta-variable. *)
     Feedback.msg_notice
-      ((Printer.pr_econstr_env env evd c_1) ++
+      ((Printer.pr_econstr_env env sigma c_1) ++
        str " has type " ++
-       (Printer.pr_econstr_env env evd the_type))
+       (Printer.pr_econstr_env env sigma the_type))
 
 
-let c_S evd =
+let c_S sigma =
   let gr = find_reference "Tuto3" ["Coq"; "Init"; "Datatypes"] "S" in
-  Evarutil.new_global evd gr
+  Evarutil.new_global sigma gr
 
-let c_O evd =
+let c_O sigma =
   let gr = find_reference "Tuto3" ["Coq"; "Init"; "Datatypes"] "O" in
-  Evarutil.new_global evd gr
+  Evarutil.new_global sigma gr
 
-let c_E evd =
+let c_E sigma =
   let gr = find_reference "Tuto3" ["Tuto3"; "Data"] "EvenNat" in
-  Evarutil.new_global evd gr
+  Evarutil.new_global sigma gr
 
-let c_D evd =
+let c_D sigma =
   let gr = find_reference "Tuto3" ["Tuto3"; "Data"] "tuto_div2" in
-  Evarutil.new_global evd gr
+  Evarutil.new_global sigma gr
 
-let c_Q evd =
+let c_Q sigma =
   let gr = find_reference "Tuto3" ["Coq"; "Init"; "Logic"] "eq" in
-  Evarutil.new_global evd gr
+  Evarutil.new_global sigma gr
 
-let c_R evd =
+let c_R sigma =
   let gr = find_reference "Tuto3" ["Coq"; "Init"; "Logic"] "eq_refl" in
-  Evarutil.new_global evd gr
+  Evarutil.new_global sigma gr
 
-let c_N evd =
+let c_N sigma =
   let gr = find_reference "Tuto3" ["Coq"; "Init"; "Datatypes"] "nat" in
-  Evarutil.new_global evd gr
+  Evarutil.new_global sigma gr
 
-let c_C evd =
+let c_C sigma =
   let gr = find_reference "Tuto3" ["Tuto3"; "Data"] "C" in
-  Evarutil.new_global evd gr
+  Evarutil.new_global sigma gr
 
-let c_F evd =
+let c_F sigma =
   let gr = find_reference "Tuto3" ["Tuto3"; "Data"] "S_ev" in
-  Evarutil.new_global evd gr
+  Evarutil.new_global sigma gr
 
-let c_P evd =
+let c_P sigma =
   let gr = find_reference "Tuto3" ["Tuto3"; "Data"] "s_half_proof" in
-  Evarutil.new_global evd gr
+  Evarutil.new_global sigma gr
 
 (* If c_S was universe polymorphic, we should have created a new constant
    at each iteration of buildup. *)
-let mk_nat evd n =
-  let evd, c_S = c_S evd in
-  let evd, c_O = c_O evd in
+let mk_nat sigma n =
+  let sigma, c_S = c_S sigma in
+  let sigma, c_O = c_O sigma in
   let rec buildup = function
     | 0 -> c_O
     | n -> EConstr.mkApp (c_S, [| buildup (n - 1) |]) in
-  if n <= 0 then evd, c_O else evd, buildup n
+  if n <= 0 then sigma, c_O else sigma, buildup n
 
 let example_classes n =
   let env = Global.env () in
-  let evd = Evd.from_env env in
-  let evd, c_n = mk_nat evd n in
-  let evd, n_half = mk_nat evd (n / 2) in
-  let evd, c_N = c_N evd in
-  let evd, c_div = c_D evd in
-  let evd, c_even = c_E evd in
-  let evd, c_Q = c_Q evd in
-  let evd, c_R = c_R evd in
+  let sigma = Evd.from_env env in
+  let sigma, c_n = mk_nat sigma n in
+  let sigma, n_half = mk_nat sigma (n / 2) in
+  let sigma, c_N = c_N sigma in
+  let sigma, c_div = c_D sigma in
+  let sigma, c_even = c_E sigma in
+  let sigma, c_Q = c_Q sigma in
+  let sigma, c_R = c_R sigma in
   let arg_type = EConstr.mkApp (c_even, [| c_n |]) in
-  let evd0 = evd in
-  let evd, instance = Evarutil.new_evar env evd arg_type in
+  let sigma0 = sigma in
+  let sigma, instance = Evarutil.new_evar env sigma arg_type in
   let c_half = EConstr.mkApp (c_div, [|c_n; instance|]) in
-  let _ = Feedback.msg_notice (Printer.pr_econstr_env env evd c_half) in
-  let evd, the_type = Typing.type_of env evd c_half in
-  let _ = Feedback.msg_notice (Printer.pr_econstr_env env evd c_half) in
+  let _ = Feedback.msg_notice (Printer.pr_econstr_env env sigma c_half) in
+  let sigma, the_type = Typing.type_of env sigma c_half in
+  let _ = Feedback.msg_notice (Printer.pr_econstr_env env sigma c_half) in
   let proved_equality =
     EConstr.mkCast(EConstr.mkApp (c_R, [| c_N; c_half |]), Constr.DEFAULTcast,
       EConstr.mkApp (c_Q, [| c_N; c_half; n_half|])) in
 (* This is where we force the system to compute with type classes. *)
 (* Question to coq developers: why do we pass two evd arguments to
-   solve_remaining_evars? Is the choice of evd0 relevant here? *)
-  let evd = Pretyping.solve_remaining_evars
-    (Pretyping.default_inference_flags true) env evd ~initial:evd0 in
-  let evd, final_type = Typing.type_of env evd proved_equality in
-  Feedback.msg_notice (Printer.pr_econstr_env env evd proved_equality)
+   solve_remaining_evars? Is the choice of sigma0 relevant here? *)
+  let sigma = Pretyping.solve_remaining_evars
+    (Pretyping.default_inference_flags true) env sigma ~initial:sigma0 in
+  let sigma, final_type = Typing.type_of env sigma proved_equality in
+  Feedback.msg_notice (Printer.pr_econstr_env env sigma proved_equality)
 
 (* This function, together with definitions in Data.v, shows how to
    trigger automatic proofs at the time of typechecking, based on
@@ -152,36 +152,36 @@ let example_classes n =
 *)
 let example_canonical n =
   let env = Global.env () in
-  let evd = Evd.from_env env in
+  let sigma = Evd.from_env env in
 (* Construct a natural representation of this integer. *)
-  let evd, c_n = mk_nat evd n in
+  let sigma, c_n = mk_nat sigma n in
 (* terms for "nat", "eq", "S_ev", "eq_refl", "C" *)
-  let evd, c_N = c_N evd in
-  let evd, c_F = c_F evd in
-  let evd, c_R = c_R evd in
-  let evd, c_C = c_C evd in
-  let evd, c_P = c_P evd in
+  let sigma, c_N = c_N sigma in
+  let sigma, c_F = c_F sigma in
+  let sigma, c_R = c_R sigma in
+  let sigma, c_C = c_C sigma in
+  let sigma, c_P = c_P sigma in
 (* the last argument of C *)
   let refl_term = EConstr.mkApp (c_R, [|c_N; c_n |]) in
 (* Now we build two existential variables, for the value of the half and for
    the "S_ev" structure that triggers the proof search. *)
-  let evd, ev1 = Evarutil.new_evar env evd c_N in
+  let sigma, ev1 = Evarutil.new_evar env sigma c_N in
 (* This is the type for the second existential variable *)
   let csev = EConstr.mkApp (c_F, [| ev1 |]) in
-  let evd, ev2 = Evarutil.new_evar env evd csev in
+  let sigma, ev2 = Evarutil.new_evar env sigma csev in
 (* Now we build the C structure. *)
   let test_term = EConstr.mkApp (c_C, [| c_n; ev1; ev2; refl_term |]) in
 (* Type-checking this term will compute values for the existential variables *)
-  let evd, final_type = Typing.type_of env evd test_term in
+  let sigma, final_type = Typing.type_of env sigma test_term in
 (* The computed type has two parameters, the second one is the proof. *)
-  let value = match EConstr.kind evd final_type with
+  let value = match EConstr.kind sigma final_type with
       | Constr.App(_, [| _; the_half |]) -> the_half
       | _ -> failwith "expecting the whole type to be \"cmp _ the_half\"" in
-  let _ = Feedback.msg_notice (Printer.pr_econstr_env env evd value) in
+  let _ = Feedback.msg_notice (Printer.pr_econstr_env env sigma value) in
 (* I wish for a nicer way to get the value of ev2 in the evar_map *)
-  let prf_struct = EConstr.of_constr (EConstr.to_constr evd ev2) in
+  let prf_struct = EConstr.of_constr (EConstr.to_constr sigma ev2) in
   let the_prf = EConstr.mkApp (c_P, [| ev1; prf_struct |]) in
-  let evd, the_statement = Typing.type_of env evd the_prf in
+  let sigma, the_statement = Typing.type_of env sigma the_prf in
   Feedback.msg_notice
-    (Printer.pr_econstr_env env evd the_prf ++ str " has type " ++
-     Printer.pr_econstr_env env evd the_statement)
+    (Printer.pr_econstr_env env sigma the_prf ++ str " has type " ++
+     Printer.pr_econstr_env env sigma the_statement)
diff --git a/doc/plugin_tutorial/tuto3/src/g_tuto3.mlg b/doc/plugin_tutorial/tuto3/src/g_tuto3.mlg
index f4d9e7fd5b..14b8eb5f07 100644
--- a/doc/plugin_tutorial/tuto3/src/g_tuto3.mlg
+++ b/doc/plugin_tutorial/tuto3/src/g_tuto3.mlg
@@ -14,13 +14,13 @@ open Stdarg
 VERNAC COMMAND EXTEND ShowTypeConstruction CLASSIFIED AS QUERY
 | [ "Tuto3_1" ] ->
   { let env = Global.env () in
-    let evd = Evd.from_env env in
-    let evd, s = Evd.new_sort_variable Evd.univ_rigid evd in
+    let sigma = Evd.from_env env in
+    let sigma, s = Evd.new_sort_variable Evd.univ_rigid sigma in
     let new_type_2 = EConstr.mkSort s in
-    let evd, _ =
+    let sigma, _ =
       Typing.type_of (Global.env()) (Evd.from_env (Global.env())) new_type_2 in
     Feedback.msg_notice
-      (Printer.pr_econstr_env env evd new_type_2) }
+      (Printer.pr_econstr_env env sigma new_type_2) }
 END
 
 VERNAC COMMAND EXTEND ShowOneConstruction CLASSIFIED AS QUERY
diff --git a/doc/plugin_tutorial/tuto3/src/tuto_tactic.ml b/doc/plugin_tutorial/tuto3/src/tuto_tactic.ml
index 2d541087ce..796a65f40d 100644
--- a/doc/plugin_tutorial/tuto3/src/tuto_tactic.ml
+++ b/doc/plugin_tutorial/tuto3/src/tuto_tactic.ml
@@ -65,10 +65,10 @@ let package i = Goal.enter begin fun gl ->
    and return the value a.  *)
 
 (* Remark by Maxime: look for destApp combinator. *)
-let unpack_type evd term =
+let unpack_type sigma term =
   let report () =
     CErrors.user_err (Pp.str "expecting a packed type") in
-  match EConstr.kind evd term with
+  match EConstr.kind sigma term with
   | Constr.App (_, [| ty |]) -> ty
   | _ -> report ()
 
@@ -76,19 +76,19 @@ let unpack_type evd term =
    A -> pack B -> C and return A, B, C
   but it is not used in the current version of our tactic.
   It is kept as an example. *)
-let two_lambda_pattern evd term =
+let two_lambda_pattern sigma term =
   let report () =
     CErrors.user_err (Pp.str "expecting two nested implications") in
 (* Note that pattern-matching is always done through the EConstr.kind function,
    which only provides one-level deep patterns. *)
-  match EConstr.kind evd term with
+  match EConstr.kind sigma term with
   (* Here we recognize the outer implication *)
   | Constr.Prod (_, ty1, l1) ->
       (* Here we recognize the inner implication *)
-      (match EConstr.kind evd l1 with
+      (match EConstr.kind sigma l1 with
       | Constr.Prod (n2, packed_ty2, deep_conclusion) ->
         (* Here we recognized that the second type is an application *)
-        ty1, unpack_type evd packed_ty2, deep_conclusion
+        ty1, unpack_type sigma packed_ty2, deep_conclusion
       | _ -> report ())
   | _ -> report ()
 
@@ -104,22 +104,22 @@ let get_type_of_hyp env id =
 
 let repackage i h_hyps_id = Goal.enter begin fun gl ->
     let env = Goal.env gl in
-    let evd = Tacmach.New.project gl in
+    let sigma = Tacmach.New.project gl in
     let concl = Tacmach.New.pf_concl gl in
     let (ty1 : EConstr.t) = get_type_of_hyp env i in
     let (packed_ty2 : EConstr.t) = get_type_of_hyp env h_hyps_id in
-    let ty2 = unpack_type evd packed_ty2 in
+    let ty2 = unpack_type sigma packed_ty2 in
     let new_packed_type = EConstr.mkApp (c_P (), [| ty1; ty2 |]) in
     let open EConstr in
     let new_packed_value =
         mkApp (c_R (), [| ty1; ty2; mkVar i;
           mkApp (c_U (), [| ty2; mkVar h_hyps_id|]) |]) in
-    Refine.refine ~typecheck:true begin fun evd ->
-      let evd, new_goal = Evarutil.new_evar env evd
+    Refine.refine ~typecheck:true begin fun sigma ->
+      let sigma, new_goal = Evarutil.new_evar env sigma
           (mkArrowR (mkApp(c_H (), [| new_packed_type |]))
              (Vars.lift 1 concl))
       in
-      evd, mkApp (new_goal,
+      sigma, mkApp (new_goal,
                   [|mkApp(c_M (), [|new_packed_type; new_packed_value |]) |])
       end
     end
diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst
index 3f966755ca..0cff987a27 100644
--- a/doc/sphinx/proof-engine/proof-handling.rst
+++ b/doc/sphinx/proof-engine/proof-handling.rst
@@ -535,19 +535,6 @@ Requesting information
             eexists ?[n].
             Show n.
 
-   .. cmdv:: Show Script
-      :name: Show Script
-
-      Displays the whole list of tactics applied from the
-      beginning of the current proof. This tactics script may contain some
-      holes (subgoals not yet proved). They are printed under the form
-
-      ``<Your Tactic Text here>``.
-
-      .. deprecated:: 8.10
-
-         Please use a text editor.
-
    .. cmdv:: Show Proof
       :name: Show Proof
 
@@ -705,9 +692,10 @@ command in CoqIDE.  You can change the background colors shown for diffs from th
 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.
+As of June 2019, Proof General can also display Coq-generated proof diffs automatically.
+Please see the PG documentation section
+"`Showing Proof Diffs" <https://proofgeneral.github.io/doc/master/userman/Coq-Proof-General#Showing-Proof-Diffs>`_)
+for details.
 
 How diffs are calculated
 ````````````````````````
diff --git a/ide/coq_commands.ml b/ide/coq_commands.ml
index b0bafb7930..7f68f24c22 100644
--- a/ide/coq_commands.ml
+++ b/ide/coq_commands.ml
@@ -126,7 +126,6 @@ let commands = [
      "Show Intros";
      "Show Programs";
      "Show Proof";
-     "Show Script";
      "Show Tree";*)
      "Structure";
      "Syntactic Definition";
@@ -221,7 +220,6 @@ let state_preserving = [
   "Show Intro";
   "Show Intros";
   "Show Proof";
-  "Show Script";
   "Show Tree";
 
   "Test Printing If";
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 216be3797b..de1b592337 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -1489,8 +1489,6 @@ let com_eqn sign uctx nb_arg eq_name functional_ref f_ref terminate_ref equation
 	       }
 	  )
        )) pstate in
-     (* (try Vernacentries.interp (Vernacexpr.VernacShow Vernacexpr.ShowProof) with _ -> ()); *)
-(*      Vernacentries.interp (Vernacexpr.VernacShow Vernacexpr.ShowScript); *)
     let _ = Flags.silently (fun () -> Lemmas.save_proof_proved ?proof:None ~pstate ~opaque:opacity ~idopt:None) () in
     ()
 (*      Pp.msgnl (fun _ _ -> str "eqn finished"); *)
diff --git a/stm/stm.ml b/stm/stm.ml
index 21f5ece244..b2bfa552b4 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -1060,99 +1060,6 @@ end = struct (* {{{ *)
 
 end (* }}} *)
 
-(* indentation code for Show Script, initially contributed
- * by D. de Rauglaudre. Should be moved away.
- *)
-
-module ShowScript = struct
-
-let indent_script_item ((ng1,ngl1),nl,beginend,ppl) (cmd,ng) =
-  (* ng1 : number of goals remaining at the current level (before cmd)
-     ngl1 : stack of previous levels with their remaining goals
-     ng : number of goals after the execution of cmd
-     beginend : special indentation stack for { } *)
-  let ngprev = List.fold_left (+) ng1 ngl1 in
-  let new_ngl =
-    if ng > ngprev then
-      (* We've branched *)
-      (ng - ngprev + 1, ng1 - 1 :: ngl1)
-    else if ng < ngprev then
-      (* A subgoal have been solved. Let's compute the new current level
-	 by discarding all levels with 0 remaining goals. *)
-      let rec loop = function
-	| (0, ng2::ngl2) -> loop (ng2,ngl2)
-	| p -> p
-      in loop (ng1-1, ngl1)
-    else
-      (* Standard case, same goal number as before *)
-      (ng1, ngl1)
-  in
-  (* When a subgoal have been solved, separate this block by an empty line *)
-  let new_nl = (ng < ngprev)
-  in
-  (* Indentation depth *)
-  let ind = List.length ngl1
-  in
-  (* Some special handling of bullets and { }, to get a nicer display *)
-  let pred n = max 0 (n-1) in
-  let ind, nl, new_beginend = match Vernacprop.under_control cmd with
-    | VernacSubproof _ -> pred ind, nl, (pred ind)::beginend
-    | VernacEndSubproof -> List.hd beginend, false, List.tl beginend
-    | VernacBullet _ -> pred ind, nl, beginend
-    | _ -> ind, nl, beginend
-  in
-  let pp = Pp.(
-    (if nl then fnl () else mt ()) ++
-    (hov (ind+1) (str (String.make ind ' ') ++ Ppvernac.pr_vernac cmd)))
-  in
-  (new_ngl, new_nl, new_beginend, pp :: ppl)
-
-let get_script prf =
-  let branch, test =
-    match prf with
-    | None -> VCS.Branch.master, fun _ -> true
-    | Some name -> VCS.current_branch (),fun nl -> nl=[] || List.mem name nl in
-  let rec find acc id =
-    if Stateid.equal id Stateid.initial ||
-       Stateid.equal id Stateid.dummy then acc else
-    let view = VCS.visit id in
-    match view.step with
-    | `Fork((_,_,_,ns), _) when test ns -> acc
-    | `Qed (qed, proof) -> find [qed.qast.expr, (VCS.get_info id).n_goals] proof
-    | `Sideff (ReplayCommand x,_) ->
-         find ((x.expr, (VCS.get_info id).n_goals)::acc) view.next
-    | `Sideff (CherryPickEnv, id)  -> find acc id
-    | `Cmd {cast = x; ctac} when ctac -> (* skip non-tactics *)
-         find ((x.expr, (VCS.get_info id).n_goals)::acc) view.next
-    | `Cmd _ -> find acc view.next
-    | `Alias (id,_) -> find acc id
-    | `Fork _ -> find acc view.next
-    in
-  find [] (VCS.get_branch_pos branch)
-
-let warn_show_script_deprecated =
-  CWarnings.create ~name:"deprecated-show-script" ~category:"deprecated"
-    (fun () -> Pp.str "The “Show Script” command is deprecated.")
-
-let show_script ?proof () =
-  warn_show_script_deprecated ();
-  try
-    let prf =
-      try match proof with
-      | None -> Some (PG_compat.get_current_proof_name ())
-      | Some (p,_) -> Some (p.Proof_global.id)
-      with PG_compat.NoCurrentProof -> None
-    in
-    let cmds = get_script prf in
-    let _,_,_,indented_cmds =
-      List.fold_left indent_script_item ((1,[]),false,[],[]) cmds
-    in
-    let indented_cmds = List.rev (indented_cmds) in
-    msg_notice Pp.(v 0 (prlist_with_sep fnl (fun x -> x) indented_cmds))
-  with Vcs_aux.Expired -> ()
-
-end
-
 (* Wrapper for Vernacentries.interp to set the feedback id *)
 (* It is currently called 19 times, this number should be certainly
    reduced... *)
@@ -1172,21 +1079,17 @@ let stm_vernac_interp ?proof ?route id st { verbose; expr } : Vernacstate.t =
     | VernacAbortAll | VernacAbort _ -> true
     | _ -> false
   in
-  let aux_interp st expr =
-    (* XXX unsupported attributes *)
-    let cmd = Vernacprop.under_control expr in
-    if is_filtered_command cmd then
-      (stm_pperr_endline Pp.(fun () -> str "ignoring " ++ Ppvernac.pr_vernac expr); st)
-    else
-      match cmd with
-      | VernacShow ShowScript -> ShowScript.show_script (); st (* XX we are ignoring control here *)
-      | _ ->
-        stm_pperr_endline Pp.(fun () -> str "interpreting " ++ Ppvernac.pr_vernac expr);
-        try Vernacentries.interp ?verbosely:(Some verbose) ?proof ~st expr
-        with e ->
-          let e = CErrors.push e in
-          Exninfo.iraise Hooks.(call_process_error_once e)
-  in aux_interp st expr
+  (* XXX unsupported attributes *)
+  let cmd = Vernacprop.under_control expr in
+  if is_filtered_command cmd then
+    (stm_pperr_endline Pp.(fun () -> str "ignoring " ++ Ppvernac.pr_vernac expr); st)
+  else begin
+    stm_pperr_endline Pp.(fun () -> str "interpreting " ++ Ppvernac.pr_vernac expr);
+    try Vernacentries.interp ?verbosely:(Some verbose) ?proof ~st expr
+    with e ->
+      let e = CErrors.push e in
+      Exninfo.iraise Hooks.(call_process_error_once e)
+  end
 
 (****************************** CRUFT *****************************************)
 (******************************************************************************)
diff --git a/vernac/g_proofs.mlg b/vernac/g_proofs.mlg
index ecc7d3ff88..ea35ea782d 100644
--- a/vernac/g_proofs.mlg
+++ b/vernac/g_proofs.mlg
@@ -88,7 +88,6 @@ GRAMMAR EXTEND Gram
       | IDENT "Show" -> { VernacShow (ShowGoal OpenSubgoals) }
       | IDENT "Show"; n = natural -> { VernacShow (ShowGoal (NthGoal n)) }
       | IDENT "Show"; id = ident -> { VernacShow (ShowGoal (GoalId id)) }
-      | IDENT "Show"; IDENT "Script" -> { VernacShow ShowScript }
       | IDENT "Show"; IDENT "Existentials" -> { VernacShow ShowExistentials }
       | IDENT "Show"; IDENT "Universes" -> { VernacShow ShowUniverses }
       | IDENT "Show"; IDENT "Conjectures" -> { VernacShow ShowProofNames }
diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml
index e307c0c268..535a0fa02c 100644
--- a/vernac/ppvernac.ml
+++ b/vernac/ppvernac.ml
@@ -628,7 +628,6 @@ open Pputils
         let pr_showable = function
           | ShowGoal n -> keyword "Show" ++ pr_goal_reference n
           | ShowProof -> keyword "Show Proof"
-          | ShowScript -> keyword "Show Script"
           | ShowExistentials -> keyword "Show Existentials"
           | ShowUniverses -> keyword "Show Universes"
           | ShowProofNames -> keyword "Show Conjectures"
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 22427621e6..337cb233a2 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -2169,7 +2169,6 @@ let vernac_show ~pstate =
     begin function
       | ShowProof -> show_proof ~pstate
       | ShowMatch id -> show_match id
-      | ShowScript -> assert false  (* Only the stm knows the script *)
       | _ ->
         user_err (str "This command requires an open proof.")
     end
@@ -2190,7 +2189,6 @@ let vernac_show ~pstate =
     | ShowIntros all -> show_intro ~pstate all
     | ShowProof -> show_proof ~pstate:(Some pstate)
     | ShowMatch id -> show_match id
-    | ShowScript -> assert false  (* Only the stm knows the script *)
     end
 
 let vernac_check_guard ~pstate =
diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml
index df1d08ad0f..b8946fad23 100644
--- a/vernac/vernacexpr.ml
+++ b/vernac/vernacexpr.ml
@@ -81,7 +81,6 @@ type locatable =
 type showable =
   | ShowGoal of goal_reference
   | ShowProof
-  | ShowScript
   | ShowExistentials
   | ShowUniverses
   | ShowProofNames