diff options
| -rw-r--r-- | doc/sphinx/proof-engine/tactics.rst | 4 | ||||
| -rw-r--r-- | plugins/ltac/extraargs.ml4 | 20 |
2 files changed, 19 insertions, 5 deletions
diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index 562f8568dc..c7f30bc331 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -1323,8 +1323,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 dbbdbfa396..8e572213bf 100644 --- a/plugins/ltac/extraargs.ml4 +++ b/plugins/ltac/extraargs.ml4 @@ -196,9 +196,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 @@ -217,6 +217,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 @@ -231,8 +239,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 |