Merge PR #8110: Fixing capital letters in the "in" syntax of instantiate.

2 files changed, 19 insertions, 5 deletions

diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst
index 241cdf5eea..62a482096c 100644
--- a/doc/sphinx/proof-engine/tactics.rst
+++ b/doc/sphinx/proof-engine/tactics.rst
@@ -1345,8 +1345,8 @@ name of the variable (here :g:`n`) is chosen based on :g:`T`.
    changes in the goal, its use is strongly discouraged.
 
 .. tacv:: instantiate ( @num := @term ) in @ident
-.. tacv:: instantiate ( @num := @term ) in ( Value of @ident )
-.. tacv:: instantiate ( @num := @term ) in ( Type of @ident )
+.. tacv:: instantiate ( @num := @term ) in ( value of @ident )
+.. tacv:: instantiate ( @num := @term ) in ( type of @ident )
 
    These allow to refer respectively to existential variables occurring in a
    hypothesis or in the body or the type of a local definition.
diff --git a/plugins/ltac/extraargs.ml4 b/plugins/ltac/extraargs.ml4
index d779951180..38600695dc 100644
--- a/plugins/ltac/extraargs.ml4
+++ b/plugins/ltac/extraargs.ml4
@@ -199,9 +199,9 @@ let pr_gen_place pr_id = function
     ConclLocation () -> Pp.mt ()
   | HypLocation (id,InHyp) -> str "in " ++ pr_id id
   | HypLocation (id,InHypTypeOnly) ->
-      str "in (Type of " ++ pr_id id ++ str ")"
+      str "in (type of " ++ pr_id id ++ str ")"
   | HypLocation (id,InHypValueOnly) ->
-      str "in (Value of " ++ pr_id id ++ str ")"
+      str "in (value of " ++ pr_id id ++ str ")"
 
 let pr_loc_place _ _ _ = pr_gen_place (fun { CAst.v = id } -> Id.print id)
 let pr_place _ _ _ = pr_gen_place Id.print
@@ -220,6 +220,14 @@ let interp_place ist gl p =
 
 let subst_place subst pl = pl
 
+let warn_deprecated_instantiate_syntax =
+  CWarnings.create ~name:"deprecated-instantiate-syntax" ~category:"deprecated"
+         (fun (v,v',id) ->
+           let s = Id.to_string id in
+           Pp.strbrk
+             ("Syntax \"in (" ^ v ^ " of " ^ s ^ ")\" is deprecated; use \"in (" ^ v' ^ " of " ^ s ^ ")\".")
+         )
+
 ARGUMENT EXTEND hloc
     PRINTED BY pr_place
     INTERPRETED BY interp_place
@@ -234,8 +242,14 @@ ARGUMENT EXTEND hloc
 | [ "in" ident(id) ] ->
     [ HypLocation ((CAst.make id),InHyp) ]
 | [ "in" "(" "Type" "of" ident(id) ")" ] ->
-    [ HypLocation ((CAst.make id),InHypTypeOnly) ]
+    [ warn_deprecated_instantiate_syntax ("Type","type",id);
+      HypLocation ((CAst.make id),InHypTypeOnly) ]
 | [ "in" "(" "Value" "of" ident(id) ")" ] ->
+    [ warn_deprecated_instantiate_syntax ("Value","value",id);
+      HypLocation ((CAst.make id),InHypValueOnly) ]
+| [ "in" "(" "type" "of" ident(id) ")" ] ->
+    [ HypLocation ((CAst.make id),InHypTypeOnly) ]
+| [ "in" "(" "value" "of" ident(id) ")" ] ->
     [ HypLocation ((CAst.make id),InHypValueOnly) ]
 
  END