diff options
36 files changed, 874 insertions, 638 deletions
diff --git a/doc/changelog/05-tactic-language/13774-ltac2-deprecated-attribute-term.rst b/doc/changelog/05-tactic-language/13774-ltac2-deprecated-attribute-term.rst new file mode 100644 index 0000000000..5fdfbd9796 --- /dev/null +++ b/doc/changelog/05-tactic-language/13774-ltac2-deprecated-attribute-term.rst @@ -0,0 +1,6 @@ +- **Added:** + Ltac2 commands defining terms now accept the :attr:`deprecated` + attribute + (`#13774 <https://github.com/coq/coq/pull/13774>`_, + fixes `#12317 <https://github.com/coq/coq/issues/12317>`_, + by Pierre-Marie Pédrot). diff --git a/doc/changelog/05-tactic-language/13914-ltac2-cast-fun-return.rst b/doc/changelog/05-tactic-language/13914-ltac2-cast-fun-return.rst new file mode 100644 index 0000000000..5ecc5934eb --- /dev/null +++ b/doc/changelog/05-tactic-language/13914-ltac2-cast-fun-return.rst @@ -0,0 +1,5 @@ +- **Added:** + Allow the presence of type casts for function return values, let bindings and + global definitions in Ltac2 + (`#13914 <https://github.com/coq/coq/pull/13914>`_, + by Pierre-Marie Pédrot). diff --git a/doc/sphinx/proof-engine/ltac2.rst b/doc/sphinx/proof-engine/ltac2.rst index 9f3f0ef3d5..294c56ef06 100644 --- a/doc/sphinx/proof-engine/ltac2.rst +++ b/doc/sphinx/proof-engine/ltac2.rst @@ -66,7 +66,6 @@ Current limitations include: - An easy way to get the number of constructors of an inductive type. Currently only way to do this is to destruct a variable of the inductive type and count the number of goals that result. -- The :attr:`deprecated` attribute is not supported for Ltac2 definitions. - Error messages may be cryptic. @@ -229,6 +228,8 @@ One can define new types with the following commands. defined in Coq and give their type information. They can also declare data structures from OCaml. This command has no use for the end user. + This command supports the :attr:`deprecated` attribute. + APIs ~~~~ @@ -263,10 +264,10 @@ There is dedicated syntax for list and array literals. .. prodn:: ltac2_expr ::= @ltac2_expr5 ; @ltac2_expr | @ltac2_expr5 - ltac2_expr5 ::= fun {+ @tac2pat0 } => @ltac2_expr + ltac2_expr5 ::= fun {+ @tac2pat0 } {? : @ltac2_type } => @ltac2_expr | let {? rec } @ltac2_let_clause {* with @ltac2_let_clause } in @ltac2_expr | @ltac2_expr3 - ltac2_let_clause ::= {+ @tac2pat0 } := @ltac2_expr + ltac2_let_clause ::= {+ @tac2pat0 } {? : @ltac2_type } := @ltac2_expr ltac2_expr3 ::= {+, @ltac2_expr2 } ltac2_expr2 ::= @ltac2_expr1 :: @ltac2_expr2 | @ltac2_expr1 @@ -304,7 +305,7 @@ Ltac2 Definitions .. insertprodn tac2def_body tac2def_body .. prodn:: - tac2def_body ::= {| _ | @ident } {* @tac2pat0 } := @ltac2_expr + tac2def_body ::= {| _ | @ident } {* @tac2pat0 } {? : @ltac2_type } := @ltac2_expr This command defines a new global Ltac2 value. If one or more :token:`tac2pat0` are specified, the new value is a function. This is a shortcut for one of the @@ -319,6 +320,8 @@ Ltac2 Definitions If ``mutable`` is set, the definition can be redefined at a later stage (see below). + This command supports the :attr:`deprecated` attribute. + .. cmd:: Ltac2 Set @qualid {? as @ident } := @ltac2_expr This command redefines a previous ``mutable`` definition. @@ -1246,6 +1249,8 @@ Notations so that you may have to resort to thunking to ensure that side-effects are performed at the right time. + This command supports the :attr:`deprecated` attribute. + Abbreviations ~~~~~~~~~~~~~ @@ -1276,6 +1281,8 @@ Abbreviations Note that abbreviations are not type checked at all, and may result in typing errors after expansion. + This command supports the :attr:`deprecated` attribute. + .. _defining_tactics: Defining tactics diff --git a/doc/sphinx/using/libraries/writing.rst b/doc/sphinx/using/libraries/writing.rst index 917edf0774..7461bfe443 100644 --- a/doc/sphinx/using/libraries/writing.rst +++ b/doc/sphinx/using/libraries/writing.rst @@ -22,13 +22,17 @@ deprecated compatibility alias using :cmd:`Notation (abbreviation)` by a comma. This attribute is supported by the following commands: :cmd:`Ltac`, - :cmd:`Tactic Notation`, :cmd:`Notation`, :cmd:`Infix`. + :cmd:`Tactic Notation`, :cmd:`Notation`, :cmd:`Infix`, :cmd:`Ltac2`, + :cmd:`Ltac2 Notation`, :cmd:`Ltac2 external`. It can trigger the following warnings: .. warn:: Tactic @qualid is deprecated since @string__since. @string__note. Tactic Notation @qualid is deprecated since @string__since. @string__note. Notation @string is deprecated since @string__since. @string__note. + Ltac2 definition @qualid is deprecated since @string__since. @string__note. + Ltac2 alias @qualid is deprecated since @string__since. @string__note. + Ltac2 notation {+ @ltac2_scope } is deprecated since @string__since. @string__note. :n:`@qualid` or :n:`@string` is the notation, :n:`@string__since` is the version number, :n:`@string__note` is diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg index 24ecc65e9b..fd1c3c0260 100644 --- a/doc/tools/docgram/common.edit_mlg +++ b/doc/tools/docgram/common.edit_mlg @@ -2730,6 +2730,7 @@ SPLICE: [ | variance_identref | rewriter | conversion +| type_cast ] (* end SPLICE *) RENAME: [ diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar index be1b9d80fb..ab1a9d4c75 100644 --- a/doc/tools/docgram/fullGrammar +++ b/doc/tools/docgram/fullGrammar @@ -1,6 +1,492 @@ (* Coq grammar generated from .mlg files. Do not edit by hand. Not compiled into Coq *) DOC_GRAMMAR +Constr.ident: [ +| Prim.ident +] + +Prim.name: [ +| "_" +] + +global: [ +| Prim.reference +] + +constr_pattern: [ +| constr +] + +cpattern: [ +| lconstr +] + +sort: [ +| "Set" +| "Prop" +| "SProp" +| "Type" +| "Type" "@{" "_" "}" +| "Type" "@{" universe "}" +] + +sort_family: [ +| "Set" +| "Prop" +| "SProp" +| "Type" +] + +universe_increment: [ +| "+" natural +| +] + +universe_name: [ +| global +| "Set" +| "Prop" +] + +universe_expr: [ +| universe_name universe_increment +] + +universe: [ +| "max" "(" LIST1 universe_expr SEP "," ")" +| universe_expr +] + +lconstr: [ +| term200 +] + +constr: [ +| term8 +| "@" global univ_annot +] + +term200: [ +| binder_constr +| term100 +] + +term100: [ +| term99 "<:" term200 +| term99 "<<:" term200 +| term99 ":" term200 +| term99 ":>" +| term99 +] + +term99: [ +| term90 +] + +term90: [ +| term10 +] + +term10: [ +| term9 LIST1 arg +| "@" global univ_annot LIST0 term9 +| "@" pattern_ident LIST1 identref +| term9 +] + +term9: [ +| ".." term0 ".." +| term8 +] + +term8: [ +| term1 +] + +term1: [ +| term0 ".(" global LIST0 arg ")" +| term0 ".(" "@" global LIST0 ( term9 ) ")" +| term0 "%" IDENT +| term0 +] + +term0: [ +| atomic_constr +| term_match +| "(" term200 ")" +| "{|" record_declaration bar_cbrace +| "{" binder_constr "}" +| "`{" term200 "}" +| test_array_opening "[" "|" array_elems "|" lconstr type_cstr test_array_closing "|" "]" univ_annot +| "`(" term200 ")" +| "ltac" ":" "(" Pltac.ltac_expr ")" +] + +array_elems: [ +| LIST0 lconstr SEP ";" +] + +record_declaration: [ +| fields_def +] + +fields_def: [ +| field_def ";" fields_def +| field_def +| +] + +field_def: [ +| global binders ":=" lconstr +] + +binder_constr: [ +| "forall" open_binders "," term200 +| "fun" open_binders "=>" term200 +| "let" name binders let_type_cstr ":=" term200 "in" term200 +| "let" "fix" fix_decl "in" term200 +| "let" "cofix" cofix_body "in" term200 +| "let" [ "(" LIST0 name SEP "," ")" | "()" ] as_return_type ":=" term200 "in" term200 +| "let" "'" pattern200 ":=" term200 "in" term200 +| "let" "'" pattern200 ":=" term200 case_type "in" term200 +| "let" "'" pattern200 "in" pattern200 ":=" term200 case_type "in" term200 +| "if" term200 as_return_type "then" term200 "else" term200 +| "fix" fix_decls +| "cofix" cofix_decls +| "if" term200 "is" ssr_dthen ssr_else (* SSR plugin *) +| "if" term200 "isn't" ssr_dthen ssr_else (* SSR plugin *) +| "let" ":" ssr_mpat ":=" lconstr "in" lconstr (* SSR plugin *) +| "let" ":" ssr_mpat ":=" lconstr ssr_rtype "in" lconstr (* SSR plugin *) +| "let" ":" ssr_mpat "in" pattern200 ":=" lconstr ssr_rtype "in" lconstr (* SSR plugin *) +] + +arg: [ +| test_lpar_id_coloneq "(" identref ":=" lconstr ")" +| term9 +] + +atomic_constr: [ +| global univ_annot +| sort +| NUMBER +| string +| "_" +| "?" "[" identref "]" +| "?" "[" pattern_ident "]" +| pattern_ident evar_instance +] + +inst: [ +| identref ":=" lconstr +] + +evar_instance: [ +| "@{" LIST1 inst SEP ";" "}" +| +] + +univ_annot: [ +| "@{" LIST0 universe_level "}" +| +] + +universe_level: [ +| "Set" +| "Prop" +| "Type" +| "_" +| global +] + +fix_decls: [ +| fix_decl +| fix_decl "with" LIST1 fix_decl SEP "with" "for" identref +] + +cofix_decls: [ +| cofix_body +| cofix_body "with" LIST1 cofix_body SEP "with" "for" identref +] + +fix_decl: [ +| identref binders_fixannot type_cstr ":=" term200 +] + +cofix_body: [ +| identref binders type_cstr ":=" term200 +] + +term_match: [ +| "match" LIST1 case_item SEP "," OPT case_type "with" branches "end" +] + +case_item: [ +| term100 OPT [ "as" name ] OPT [ "in" pattern200 ] +] + +case_type: [ +| "return" term100 +] + +as_return_type: [ +| OPT [ OPT [ "as" name ] case_type ] +] + +branches: [ +| OPT "|" LIST0 eqn SEP "|" +] + +mult_pattern: [ +| LIST1 pattern200 SEP "," +] + +eqn: [ +| LIST1 mult_pattern SEP "|" "=>" lconstr +] + +record_pattern: [ +| global ":=" pattern200 +] + +record_patterns: [ +| record_pattern ";" record_patterns +| record_pattern +| +] + +pattern200: [ +| pattern100 +] + +pattern100: [ +| pattern99 ":" term200 +| pattern99 +] + +pattern99: [ +| pattern90 +] + +pattern90: [ +| pattern10 +] + +pattern10: [ +| pattern1 "as" name +| pattern1 LIST1 pattern1 +| "@" Prim.reference LIST0 pattern1 +| pattern1 +] + +pattern1: [ +| pattern0 "%" IDENT +| pattern0 +] + +pattern0: [ +| Prim.reference +| "{|" record_patterns bar_cbrace +| "_" +| "(" pattern200 ")" +| "(" pattern200 "|" LIST1 pattern200 SEP "|" ")" +| NUMBER +| string +] + +fixannot: [ +| "{" "struct" identref "}" +| "{" "wf" constr identref "}" +| "{" "measure" constr OPT identref OPT constr "}" +] + +binders_fixannot: [ +| ensure_fixannot fixannot +| binder binders_fixannot +| +] + +open_binders: [ +| name LIST0 name ":" lconstr +| name LIST0 name binders +| name ".." name +| closed_binder binders +] + +binders: [ +| LIST0 binder +| Pcoq.Constr.binders +] + +binder: [ +| name +| closed_binder +] + +closed_binder: [ +| "(" name LIST1 name ":" lconstr ")" +| "(" name ":" lconstr ")" +| "(" name ":=" lconstr ")" +| "(" name ":" lconstr ":=" lconstr ")" +| "{" name "}" +| "{" name LIST1 name ":" lconstr "}" +| "{" name ":" lconstr "}" +| "{" name LIST1 name "}" +| "[" name "]" +| "[" name LIST1 name ":" lconstr "]" +| "[" name ":" lconstr "]" +| "[" name LIST1 name "]" +| "`(" LIST1 typeclass_constraint SEP "," ")" +| "`{" LIST1 typeclass_constraint SEP "," "}" +| "`[" LIST1 typeclass_constraint SEP "," "]" +| "'" pattern0 +| [ "of" | "&" ] term99 (* SSR plugin *) +] + +one_open_binder: [ +| name +| name ":" lconstr +| one_closed_binder +] + +one_closed_binder: [ +| "(" name ":" lconstr ")" +| "{" name "}" +| "{" name ":" lconstr "}" +| "[" name "]" +| "[" name ":" lconstr "]" +| "'" pattern0 +] + +typeclass_constraint: [ +| "!" term200 +| "{" name "}" ":" [ "!" | ] term200 +| test_name_colon name ":" [ "!" | ] term200 +| term200 +] + +type_cstr: [ +| ":" lconstr +| +] + +let_type_cstr: [ +| OPT [ ":" lconstr ] +] + +preident: [ +| IDENT +] + +ident: [ +| IDENT +] + +pattern_ident: [ +| LEFTQMARK ident +] + +identref: [ +| ident +] + +hyp: [ +| identref +] + +field: [ +| FIELD +] + +fields: [ +| field fields +| field +] + +fullyqualid: [ +| ident fields +| ident +] + +name: [ +| "_" +| ident +] + +reference: [ +| ident fields +| ident +] + +qualid: [ +| reference +] + +by_notation: [ +| ne_string OPT [ "%" IDENT ] +] + +smart_global: [ +| reference +| by_notation +] + +ne_string: [ +| STRING +] + +ne_lstring: [ +| ne_string +] + +dirpath: [ +| ident LIST0 field +] + +string: [ +| STRING +] + +lstring: [ +| string +] + +integer: [ +| bigint +] + +natural: [ +| bignat +] + +bigint: [ +| bignat +| test_minus_nat "-" bignat +] + +bignat: [ +| NUMBER +] + +bar_cbrace: [ +| test_pipe_closedcurly "|" "}" +] + +strategy_level: [ +| "expand" +| "opaque" +| integer +| "transparent" +] + +vernac_toplevel: [ +| "Drop" "." +| "Quit" "." +| "BackTo" natural "." +| test_show_goal "Show" "Goal" natural "at" natural "." +| "Show" "Proof" "Diffs" OPT "removed" "." +| Pvernac.Vernac_.main_entry +] + opt_hintbases: [ | | ":" LIST1 IDENT @@ -981,492 +1467,6 @@ binder_interp: [ | "as" "strict" "pattern" ] -vernac_toplevel: [ -| "Drop" "." -| "Quit" "." -| "BackTo" natural "." -| test_show_goal "Show" "Goal" natural "at" natural "." -| "Show" "Proof" "Diffs" OPT "removed" "." -| Pvernac.Vernac_.main_entry -] - -Constr.ident: [ -| Prim.ident -] - -Prim.name: [ -| "_" -] - -global: [ -| Prim.reference -] - -constr_pattern: [ -| constr -] - -cpattern: [ -| lconstr -] - -sort: [ -| "Set" -| "Prop" -| "SProp" -| "Type" -| "Type" "@{" "_" "}" -| "Type" "@{" universe "}" -] - -sort_family: [ -| "Set" -| "Prop" -| "SProp" -| "Type" -] - -universe_increment: [ -| "+" natural -| -] - -universe_name: [ -| global -| "Set" -| "Prop" -] - -universe_expr: [ -| universe_name universe_increment -] - -universe: [ -| "max" "(" LIST1 universe_expr SEP "," ")" -| universe_expr -] - -lconstr: [ -| term200 -] - -constr: [ -| term8 -| "@" global univ_annot -] - -term200: [ -| binder_constr -| term100 -] - -term100: [ -| term99 "<:" term200 -| term99 "<<:" term200 -| term99 ":" term200 -| term99 ":>" -| term99 -] - -term99: [ -| term90 -] - -term90: [ -| term10 -] - -term10: [ -| term9 LIST1 arg -| "@" global univ_annot LIST0 term9 -| "@" pattern_ident LIST1 identref -| term9 -] - -term9: [ -| ".." term0 ".." -| term8 -] - -term8: [ -| term1 -] - -term1: [ -| term0 ".(" global LIST0 arg ")" -| term0 ".(" "@" global LIST0 ( term9 ) ")" -| term0 "%" IDENT -| term0 -] - -term0: [ -| atomic_constr -| term_match -| "(" term200 ")" -| "{|" record_declaration bar_cbrace -| "{" binder_constr "}" -| "`{" term200 "}" -| test_array_opening "[" "|" array_elems "|" lconstr type_cstr test_array_closing "|" "]" univ_annot -| "`(" term200 ")" -| "ltac" ":" "(" Pltac.ltac_expr ")" -] - -array_elems: [ -| LIST0 lconstr SEP ";" -] - -record_declaration: [ -| fields_def -] - -fields_def: [ -| field_def ";" fields_def -| field_def -| -] - -field_def: [ -| global binders ":=" lconstr -] - -binder_constr: [ -| "forall" open_binders "," term200 -| "fun" open_binders "=>" term200 -| "let" name binders let_type_cstr ":=" term200 "in" term200 -| "let" "fix" fix_decl "in" term200 -| "let" "cofix" cofix_body "in" term200 -| "let" [ "(" LIST0 name SEP "," ")" | "()" ] as_return_type ":=" term200 "in" term200 -| "let" "'" pattern200 ":=" term200 "in" term200 -| "let" "'" pattern200 ":=" term200 case_type "in" term200 -| "let" "'" pattern200 "in" pattern200 ":=" term200 case_type "in" term200 -| "if" term200 as_return_type "then" term200 "else" term200 -| "fix" fix_decls -| "cofix" cofix_decls -| "if" term200 "is" ssr_dthen ssr_else (* SSR plugin *) -| "if" term200 "isn't" ssr_dthen ssr_else (* SSR plugin *) -| "let" ":" ssr_mpat ":=" lconstr "in" lconstr (* SSR plugin *) -| "let" ":" ssr_mpat ":=" lconstr ssr_rtype "in" lconstr (* SSR plugin *) -| "let" ":" ssr_mpat "in" pattern200 ":=" lconstr ssr_rtype "in" lconstr (* SSR plugin *) -] - -arg: [ -| test_lpar_id_coloneq "(" identref ":=" lconstr ")" -| term9 -] - -atomic_constr: [ -| global univ_annot -| sort -| NUMBER -| string -| "_" -| "?" "[" identref "]" -| "?" "[" pattern_ident "]" -| pattern_ident evar_instance -] - -inst: [ -| identref ":=" lconstr -] - -evar_instance: [ -| "@{" LIST1 inst SEP ";" "}" -| -] - -univ_annot: [ -| "@{" LIST0 universe_level "}" -| -] - -universe_level: [ -| "Set" -| "Prop" -| "Type" -| "_" -| global -] - -fix_decls: [ -| fix_decl -| fix_decl "with" LIST1 fix_decl SEP "with" "for" identref -] - -cofix_decls: [ -| cofix_body -| cofix_body "with" LIST1 cofix_body SEP "with" "for" identref -] - -fix_decl: [ -| identref binders_fixannot type_cstr ":=" term200 -] - -cofix_body: [ -| identref binders type_cstr ":=" term200 -] - -term_match: [ -| "match" LIST1 case_item SEP "," OPT case_type "with" branches "end" -] - -case_item: [ -| term100 OPT [ "as" name ] OPT [ "in" pattern200 ] -] - -case_type: [ -| "return" term100 -] - -as_return_type: [ -| OPT [ OPT [ "as" name ] case_type ] -] - -branches: [ -| OPT "|" LIST0 eqn SEP "|" -] - -mult_pattern: [ -| LIST1 pattern200 SEP "," -] - -eqn: [ -| LIST1 mult_pattern SEP "|" "=>" lconstr -] - -record_pattern: [ -| global ":=" pattern200 -] - -record_patterns: [ -| record_pattern ";" record_patterns -| record_pattern -| -] - -pattern200: [ -| pattern100 -] - -pattern100: [ -| pattern99 ":" term200 -| pattern99 -] - -pattern99: [ -| pattern90 -] - -pattern90: [ -| pattern10 -] - -pattern10: [ -| pattern1 "as" name -| pattern1 LIST1 pattern1 -| "@" Prim.reference LIST0 pattern1 -| pattern1 -] - -pattern1: [ -| pattern0 "%" IDENT -| pattern0 -] - -pattern0: [ -| Prim.reference -| "{|" record_patterns bar_cbrace -| "_" -| "(" pattern200 ")" -| "(" pattern200 "|" LIST1 pattern200 SEP "|" ")" -| NUMBER -| string -] - -fixannot: [ -| "{" "struct" identref "}" -| "{" "wf" constr identref "}" -| "{" "measure" constr OPT identref OPT constr "}" -] - -binders_fixannot: [ -| ensure_fixannot fixannot -| binder binders_fixannot -| -] - -open_binders: [ -| name LIST0 name ":" lconstr -| name LIST0 name binders -| name ".." name -| closed_binder binders -] - -binders: [ -| LIST0 binder -| Pcoq.Constr.binders -] - -binder: [ -| name -| closed_binder -] - -closed_binder: [ -| "(" name LIST1 name ":" lconstr ")" -| "(" name ":" lconstr ")" -| "(" name ":=" lconstr ")" -| "(" name ":" lconstr ":=" lconstr ")" -| "{" name "}" -| "{" name LIST1 name ":" lconstr "}" -| "{" name ":" lconstr "}" -| "{" name LIST1 name "}" -| "[" name "]" -| "[" name LIST1 name ":" lconstr "]" -| "[" name ":" lconstr "]" -| "[" name LIST1 name "]" -| "`(" LIST1 typeclass_constraint SEP "," ")" -| "`{" LIST1 typeclass_constraint SEP "," "}" -| "`[" LIST1 typeclass_constraint SEP "," "]" -| "'" pattern0 -| [ "of" | "&" ] term99 (* SSR plugin *) -] - -one_open_binder: [ -| name -| name ":" lconstr -| one_closed_binder -] - -one_closed_binder: [ -| "(" name ":" lconstr ")" -| "{" name "}" -| "{" name ":" lconstr "}" -| "[" name "]" -| "[" name ":" lconstr "]" -| "'" pattern0 -] - -typeclass_constraint: [ -| "!" term200 -| "{" name "}" ":" [ "!" | ] term200 -| test_name_colon name ":" [ "!" | ] term200 -| term200 -] - -type_cstr: [ -| ":" lconstr -| -] - -let_type_cstr: [ -| OPT [ ":" lconstr ] -] - -preident: [ -| IDENT -] - -ident: [ -| IDENT -] - -pattern_ident: [ -| LEFTQMARK ident -] - -identref: [ -| ident -] - -hyp: [ -| identref -] - -field: [ -| FIELD -] - -fields: [ -| field fields -| field -] - -fullyqualid: [ -| ident fields -| ident -] - -name: [ -| "_" -| ident -] - -reference: [ -| ident fields -| ident -] - -qualid: [ -| reference -] - -by_notation: [ -| ne_string OPT [ "%" IDENT ] -] - -smart_global: [ -| reference -| by_notation -] - -ne_string: [ -| STRING -] - -ne_lstring: [ -| ne_string -] - -dirpath: [ -| ident LIST0 field -] - -string: [ -| STRING -] - -lstring: [ -| string -] - -integer: [ -| bigint -] - -natural: [ -| bignat -] - -bigint: [ -| bignat -| test_minus_nat "-" bignat -] - -bignat: [ -| NUMBER -] - -bar_cbrace: [ -| test_pipe_closedcurly "|" "}" -] - -strategy_level: [ -| "expand" -| "opaque" -| integer -| "transparent" -] - simple_tactic: [ | "btauto" | "congruence" @@ -3283,7 +3283,7 @@ ltac2_expr6: [ ] ltac2_expr5: [ -| "fun" LIST1 G_LTAC2_input_fun "=>" ltac2_expr6 (* Ltac2 plugin *) +| "fun" LIST1 G_LTAC2_input_fun type_cast "=>" ltac2_expr6 (* Ltac2 plugin *) | "let" rec_flag LIST1 G_LTAC2_let_clause SEP "with" "in" ltac2_expr6 (* Ltac2 plugin *) | "match" ltac2_expr5 "with" G_LTAC2_branches "end" (* Ltac2 plugin *) | "if" ltac2_expr5 "then" ltac2_expr5 "else" ltac2_expr5 (* Ltac2 plugin *) @@ -3371,8 +3371,13 @@ tac2expr_in_env: [ | ltac2_expr6 (* Ltac2 plugin *) ] +type_cast: [ +| (* Ltac2 plugin *) +| ":" ltac2_type5 (* Ltac2 plugin *) +] + G_LTAC2_let_clause: [ -| let_binder ":=" ltac2_expr6 (* Ltac2 plugin *) +| let_binder type_cast ":=" ltac2_expr6 (* Ltac2 plugin *) ] let_binder: [ @@ -3415,7 +3420,7 @@ G_LTAC2_input_fun: [ ] tac2def_body: [ -| G_LTAC2_binder LIST0 G_LTAC2_input_fun ":=" ltac2_expr6 (* Ltac2 plugin *) +| G_LTAC2_binder LIST0 G_LTAC2_input_fun type_cast ":=" ltac2_expr6 (* Ltac2 plugin *) ] tac2def_val: [ diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar index 5674d28139..5b19b7fc55 100644 --- a/doc/tools/docgram/orderedGrammar +++ b/doc/tools/docgram/orderedGrammar @@ -2274,7 +2274,7 @@ ltac2_entry: [ ] tac2def_body: [ -| [ "_" | ident ] LIST0 tac2pat0 ":=" ltac2_expr (* Ltac2 plugin *) +| [ "_" | ident ] LIST0 tac2pat0 OPT ( ":" ltac2_type ) ":=" ltac2_expr (* Ltac2 plugin *) ] tac2typ_def: [ @@ -2315,13 +2315,13 @@ ltac2_expr: [ ] ltac2_expr5: [ -| "fun" LIST1 tac2pat0 "=>" ltac2_expr (* Ltac2 plugin *) +| "fun" LIST1 tac2pat0 OPT ( ":" ltac2_type ) "=>" ltac2_expr (* Ltac2 plugin *) | "let" OPT "rec" ltac2_let_clause LIST0 ( "with" ltac2_let_clause ) "in" ltac2_expr (* Ltac2 plugin *) | ltac2_expr3 (* Ltac2 plugin *) ] ltac2_let_clause: [ -| LIST1 tac2pat0 ":=" ltac2_expr (* Ltac2 plugin *) +| LIST1 tac2pat0 OPT ( ":" ltac2_type ) ":=" ltac2_expr (* Ltac2 plugin *) ] ltac2_expr3: [ diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c index 704eb1ef98..27287205f4 100644 --- a/kernel/byterun/coq_interp.c +++ b/kernel/byterun/coq_interp.c @@ -230,6 +230,12 @@ if (sp - num_args < coq_stack_threshold) { \ *sp = swap_accu_sp_tmp__; \ }while(0) +/* Turn a code pointer into a stack value usable as a return address, and conversely. + The least significant bit is set to 1 so that the GC does not mistake return + addresses for heap pointers. */ +#define StoreRA(p) ((value)(p) + 1) +#define LoadRA(p) ((code_t)((value)(p) - 1)) + #if OCAML_VERSION < 41000 /* For signal handling, we hijack some code from the caml runtime */ @@ -445,7 +451,7 @@ value coq_interprete Instruct(PUSH_RETADDR) { print_instr("PUSH_RETADDR"); sp -= 3; - sp[0] = (value) (pc + *pc); + sp[0] = StoreRA(pc + *pc); sp[1] = coq_env; sp[2] = Val_long(coq_extra_args); coq_extra_args = 0; @@ -466,7 +472,7 @@ value coq_interprete arg1 = sp[0]; sp -= 3; sp[0] = arg1; - sp[1] = (value)pc; + sp[1] = StoreRA(pc); sp[2] = coq_env; sp[3] = Val_long(coq_extra_args); print_instr("call stack="); @@ -489,7 +495,7 @@ value coq_interprete sp -= 3; sp[0] = arg1; sp[1] = arg2; - sp[2] = (value)pc; + sp[2] = StoreRA(pc); sp[3] = coq_env; sp[4] = Val_long(coq_extra_args); pc = Code_val(accu); @@ -511,7 +517,7 @@ value coq_interprete sp[0] = arg1; sp[1] = arg2; sp[2] = arg3; - sp[3] = (value)pc; + sp[3] = StoreRA(pc); sp[4] = coq_env; sp[5] = Val_long(coq_extra_args); pc = Code_val(accu); @@ -531,7 +537,7 @@ value coq_interprete sp[1] = arg2; sp[2] = arg3; sp[3] = arg4; - sp[4] = (value)pc; + sp[4] = StoreRA(pc); sp[5] = coq_env; sp[6] = Val_long(coq_extra_args); pc = Code_val(accu); @@ -647,7 +653,7 @@ value coq_interprete coq_env = accu; } else { print_instr("extra args = 0"); - pc = (code_t)(sp[0]); + pc = LoadRA(sp[0]); coq_env = sp[1]; coq_extra_args = Long_val(sp[2]); sp += 3; @@ -682,7 +688,7 @@ value coq_interprete for (i = 0; i < num_args; i++) Field(accu, i + 3) = sp[i]; Code_val(accu) = pc - 3; /* Point to the preceding RESTART instr. */ sp += num_args; - pc = (code_t)(sp[0]); + pc = LoadRA(sp[0]); coq_env = sp[1]; coq_extra_args = Long_val(sp[2]); sp += 3; @@ -707,7 +713,7 @@ value coq_interprete Field(accu, 2) = coq_env; for (i = 0; i < num_args; i++) Field(accu, i + 3) = sp[i]; sp += num_args; - pc = (code_t)(sp[0]); + pc = LoadRA(sp[0]); coq_env = sp[1]; coq_extra_args = Long_val(sp[2]); sp += 3; @@ -745,7 +751,7 @@ value coq_interprete Code_val(block) = accumulate; Field(block, 1) = Val_int(2); accu = block; - pc = (code_t)(sp[0]); + pc = LoadRA(sp[0]); coq_env = sp[1]; coq_extra_args = Long_val(sp[2]); sp += 3; @@ -1031,7 +1037,7 @@ value coq_interprete mlsize_t i, nargs; sp -= 2; // Push the current instruction as the return address - sp[0] = (value)(pc - 1); + sp[0] = StoreRA(pc - 1); sp[1] = coq_env; coq_env = Field(accu, 0); // Pointer to suspension accu = sp[2]; // Save accumulator to accu register @@ -1142,7 +1148,7 @@ value coq_interprete for (i = size; i < sz; ++i) caml_initialize(&Field(accu, i), *sp++); } - pc = (code_t)(sp[0]); + pc = LoadRA(sp[0]); coq_env = sp[1]; coq_extra_args = Long_val(sp[2]); sp += 3; @@ -1160,7 +1166,7 @@ value coq_interprete sp-=2; pc++; // Push the return address - sp[0] = (value) (pc + *pc); + sp[0] = StoreRA(pc + *pc); sp[1] = coq_env; coq_env = Field(accu,0); // Pointer to suspension accu = sp[2]; // Save accumulator to accu register @@ -1263,7 +1269,7 @@ value coq_interprete } Code_val(accu) = accumulate; Field(accu, 1) = Val_int(2); - pc = (code_t)(sp[0]); + pc = LoadRA(sp[0]); coq_env = sp[1]; coq_extra_args = Long_val(sp[2]); sp += 3; @@ -1916,7 +1922,7 @@ value coq_push_ra(value code) { code_t tcode = Code_val(code); print_instr("push_ra"); coq_sp -= 3; - coq_sp[0] = (value) tcode; + coq_sp[0] = StoreRA(tcode); coq_sp[1] = Val_unit; coq_sp[2] = Val_long(0); return Val_unit; diff --git a/kernel/byterun/coq_memory.c b/kernel/byterun/coq_memory.c index a55ff57c8d..f404cb2b1c 100644 --- a/kernel/byterun/coq_memory.c +++ b/kernel/byterun/coq_memory.c @@ -66,10 +66,6 @@ static void coq_scan_roots(scanning_action action) /* Scan the stack */ for (i = coq_sp; i < coq_stack_high; i++) { if (!Is_block(*i)) continue; -#ifdef NO_NAKED_POINTERS - /* The VM stack may contain C-allocated bytecode */ - if (!Is_in_heap_or_young(*i)) continue; -#endif (*action) (*i, i); }; /* Hook */ diff --git a/lib/cProfile.ml b/lib/cProfile.ml index a4f2da7080..b68d35d2d4 100644 --- a/lib/cProfile.ml +++ b/lib/cProfile.ml @@ -285,7 +285,7 @@ let format_profile (table, outside, total) = Printf.printf "%-23s %9s %9s %10s %10s %10s\n" "Function name" "Own time" "Tot. time" "Own alloc" "Tot. alloc" "Calls "; - let l = List.sort (fun (_,{tottime=p}) (_,{tottime=p'}) -> p' - p) table in + let l = List.sort (fun p p' -> (snd p').tottime - (snd p).tottime) table in List.iter (fun (name,e) -> Printf.printf "%-23s %9.2f %9.2f %10.0f %10.0f %6d %6d\n" diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml index da4a50b674..cfdaac710b 100644 --- a/plugins/extraction/mlutil.ml +++ b/plugins/extraction/mlutil.ml @@ -217,13 +217,13 @@ module Mlenv = struct (* Adding a type with no [Tvar], hence no generalization needed. *) - let push_type {env=e;free=f} t = - { env = (0,t) :: e; free = find_free f t} + let push_type mle t = + { env = (0,t) :: mle.env; free = find_free mle.free t} (* Adding a type with no [Tvar] nor [Tmeta]. *) - let push_std_type {env=e;free=f} t = - { env = (0,t) :: e; free = f} + let push_std_type mle t = + { env = (0,t) :: mle.env; free = mle.free} end diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index 54d7c310aa..da95869abb 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -1180,7 +1180,7 @@ and eval_tactic_ist ist tac : unit Proofview.tactic = match tac with | TacSolve l -> Tacticals.New.tclSOLVE (List.map (interp_tactic ist) l) | TacComplete tac -> Tacticals.New.tclCOMPLETE (interp_tactic ist tac) | TacArg {CAst.loc} -> Ftactic.run (val_interp (ensure_loc loc ist) tac) (fun v -> tactic_of_value ist v) - | TacSelect (sel, tac) -> Tacticals.New.tclSELECT sel (interp_tactic ist tac) + | TacSelect (sel, tac) -> Goal_select.tclSELECT sel (interp_tactic ist tac) (* For extensions *) | TacAlias {loc; v=(s,l)} -> let alias = Tacenv.interp_alias s in diff --git a/proofs/goal_select.ml b/proofs/goal_select.ml index e847535aaf..68646c93c9 100644 --- a/proofs/goal_select.ml +++ b/proofs/goal_select.ml @@ -57,3 +57,22 @@ let get_default_goal_selector = ~value:(SelectNth 1) parse_goal_selector (fun v -> Pp.string_of_ppcmds @@ pr_goal_selector v) + +(* Select a subset of the goals *) +let tclSELECT ?nosuchgoal g tac = match g with + | SelectNth i -> Proofview.tclFOCUS ?nosuchgoal i i tac + | SelectList l -> Proofview.tclFOCUSLIST ?nosuchgoal l tac + | SelectId id -> Proofview.tclFOCUSID ?nosuchgoal id tac + | SelectAll -> tac + | SelectAlreadyFocused -> + let open Proofview.Notations in + Proofview.numgoals >>= fun n -> + if n == 1 then tac + else + let e = CErrors.UserError + (None, + Pp.(str "Expected a single focused goal but " ++ + int n ++ str " goals are focused.")) + in + let info = Exninfo.reify () in + Proofview.tclZERO ~info e diff --git a/proofs/goal_select.mli b/proofs/goal_select.mli index 977392baa6..c6726300f0 100644 --- a/proofs/goal_select.mli +++ b/proofs/goal_select.mli @@ -24,3 +24,5 @@ type t = val pr_goal_selector : t -> Pp.t val get_default_goal_selector : unit -> t + +val tclSELECT : ?nosuchgoal:'a Proofview.tactic -> t -> 'a Proofview.tactic -> 'a Proofview.tactic diff --git a/proofs/proof.ml b/proofs/proof.ml index 50a0e63700..e535536472 100644 --- a/proofs/proof.ml +++ b/proofs/proof.ml @@ -538,25 +538,7 @@ let solve ?with_end_tac gi info_lvl tac pr = let info = Exninfo.reify () in Proofview.tclZERO ~info (SuggestNoSuchGoals (1,pr)) in - let tac = let open Goal_select in match gi with - | SelectAlreadyFocused -> - let open Proofview.Notations in - Proofview.numgoals >>= fun n -> - if n == 1 then tac - else - let e = CErrors.UserError - (None, - Pp.(str "Expected a single focused goal but " ++ - int n ++ str " goals are focused.")) - in - let info = Exninfo.reify () in - Proofview.tclZERO ~info e - - | SelectNth i -> Proofview.tclFOCUS ~nosuchgoal i i tac - | SelectList l -> Proofview.tclFOCUSLIST ~nosuchgoal l tac - | SelectId id -> Proofview.tclFOCUSID ~nosuchgoal id tac - | SelectAll -> tac - in + let tac = Goal_select.tclSELECT ~nosuchgoal gi tac in let tac = if use_unification_heuristics () then Proofview.tclTHEN tac Refine.solve_constraints diff --git a/proofs/proofs.mllib b/proofs/proofs.mllib index 5f19c1bb09..43cde83e58 100644 --- a/proofs/proofs.mllib +++ b/proofs/proofs.mllib @@ -2,9 +2,9 @@ Miscprint Goal Evar_refiner Refine +Goal_select Proof Logic -Goal_select Proof_bullet Tacmach Clenv diff --git a/stm/stm.ml b/stm/stm.ml index 5ed6adbd63..9480bbdc2e 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -2565,8 +2565,8 @@ let get_allow_nested_proofs = ~value:false (** [process_transaction] adds a node in the document *) -let process_transaction ~doc ?(newtip=Stateid.fresh ()) - ({ verbose; expr } as x) c = +let process_transaction ~doc ?(newtip=Stateid.fresh ()) x c = + let { verbose; expr } = x in stm_pperr_endline (fun () -> str "{{{ processing: " ++ pr_ast x); let vcs = VCS.backup () in try diff --git a/stm/tQueue.ml b/stm/tQueue.ml index e17c3a2f88..2aaca85582 100644 --- a/stm/tQueue.ml +++ b/stm/tQueue.ml @@ -27,21 +27,23 @@ end = struct let create () = ref ([],sort_timestamp) let is_empty t = fst !t = [] let exists p t = List.exists (fun (_,x) -> p x) (fst !t) - let pop ?(picky=(fun _ -> true)) ({ contents = (l, rel) } as t) = + let pop ?(picky=(fun _ -> true)) t = + let (l, rel) = !t in let rec aux acc = function | [] -> raise Queue.Empty | (_,x) :: xs when picky x -> t := (List.rev acc @ xs, rel); x | (_,x) as hd :: xs -> aux (hd :: acc) xs in aux [] l - let push ({ contents = (xs, rel) } as t) x = + let push t x = + let (xs, rel) = !t in incr age; (* re-roting the whole list is not the most efficient way... *) t := (List.sort rel (xs @ [!age,x]), rel) - let clear ({ contents = (l, rel) } as t) = t := ([], rel) - let set_rel rel ({ contents = (xs, _) } as t) = + let clear t = t := ([], snd !t) + let set_rel rel t = let rel (_,x) (_,y) = rel x y in - t := (List.sort rel xs, rel) - let length ({ contents = (l, _) }) = List.length l + t := (List.sort rel (fst !t), rel) + let length t = List.length (fst !t) end type 'a t = { @@ -64,9 +66,8 @@ let create () = { release = false; } -let pop ?(picky=(fun _ -> true)) ?(destroy=ref false) - ({ queue = q; lock = m; cond = c; cond_waiting = cn } as tq) -= +let pop ?(picky=(fun _ -> true)) ?(destroy=ref false) tq = + let { queue = q; lock = m; cond = c; cond_waiting = cn } = tq in Mutex.lock m; if tq.release then (Mutex.unlock m; raise BeingDestroyed); while not (PriorityQueue.exists picky q || !destroy) do @@ -83,12 +84,14 @@ let pop ?(picky=(fun _ -> true)) ?(destroy=ref false) Mutex.unlock m; x -let broadcast { lock = m; cond = c } = +let broadcast tq = + let { lock = m; cond = c } = tq in Mutex.lock m; Condition.broadcast c; Mutex.unlock m -let push { queue = q; lock = m; cond = c; release } x = +let push tq x = + let { queue = q; lock = m; cond = c; release } = tq in if release then CErrors.anomaly(Pp.str "TQueue.push while being destroyed! Only 1 producer/destroyer allowed."); Mutex.lock m; @@ -96,18 +99,21 @@ let push { queue = q; lock = m; cond = c; release } x = Condition.broadcast c; Mutex.unlock m -let length { queue = q; lock = m } = +let length tq = + let { queue = q; lock = m } = tq in Mutex.lock m; let n = PriorityQueue.length q in Mutex.unlock m; n -let clear { queue = q; lock = m; cond = c } = +let clear tq = + let { queue = q; lock = m; cond = c } = tq in Mutex.lock m; PriorityQueue.clear q; Mutex.unlock m -let clear_saving { queue = q; lock = m; cond = c } f = +let clear_saving tq f = + let { queue = q; lock = m; cond = c } = tq in Mutex.lock m; let saved = ref [] in while not (PriorityQueue.is_empty q) do @@ -119,7 +125,7 @@ let clear_saving { queue = q; lock = m; cond = c } f = Mutex.unlock m; List.rev !saved -let is_empty { queue = q } = PriorityQueue.is_empty q +let is_empty tq = PriorityQueue.is_empty tq.queue let destroy tq = tq.release <- true; diff --git a/tactics/cbn.ml b/tactics/cbn.ml index 99d579f5c6..c3c61f6e51 100644 --- a/tactics/cbn.ml +++ b/tactics/cbn.ml @@ -453,7 +453,7 @@ let magically_constant_of_fixbody env sigma reference bd = function | None -> bd end -let contract_cofix ~env sigma ?reference (bodynum,(names,types,bodies as typedbodies)) = +let contract_cofix env sigma ?reference (bodynum,(names,types,bodies as typedbodies)) = let nbodies = Array.length bodies in let make_Fi j = let ind = nbodies-j-1 in @@ -469,7 +469,7 @@ let contract_cofix ~env sigma ?reference (bodynum,(names,types,bodies as typedbo (** Similar to the "fix" case below *) let reduce_and_refold_cofix recfun env sigma cst_l cofix sk = let raw_answer = - contract_cofix ~env sigma ?reference:(Cst_stack.reference sigma cst_l) cofix in + contract_cofix env sigma ?reference:(Cst_stack.reference sigma cst_l) cofix in apply_subst (fun sigma x (t,sk') -> let t' = Cst_stack.best_replace sigma (mkCoFix cofix) cst_l t in @@ -479,7 +479,7 @@ let reduce_and_refold_cofix recfun env sigma cst_l cofix sk = (* contracts fix==FIX[nl;i](A1...Ak;[F1...Fk]{B1....Bk}) to produce Bi[Fj --> FIX[nl;j](A1...Ak;[F1...Fk]{B1...Bk})] *) -let contract_fix ~env sigma ?reference ((recindices,bodynum),(names,types,bodies as typedbodies)) = +let contract_fix env sigma ?reference ((recindices,bodynum),(names,types,bodies as typedbodies)) = let nbodies = Array.length recindices in let make_Fi j = let ind = nbodies-j-1 in @@ -498,7 +498,7 @@ let contract_fix ~env sigma ?reference ((recindices,bodynum),(names,types,bodies context" in contract_fix *) let reduce_and_refold_fix recfun env sigma cst_l fix sk = let raw_answer = - contract_fix ~env sigma ?reference:(Cst_stack.reference sigma cst_l) fix in + contract_fix env sigma ?reference:(Cst_stack.reference sigma cst_l) fix in apply_subst (fun sigma x (t,sk') -> let t' = Cst_stack.best_replace sigma (mkFix fix) cst_l t in diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index 68afd9a128..2d69047d1e 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -683,15 +683,6 @@ module New = struct let tclPROGRESS t = Proofview.tclINDEPENDENT (Proofview.tclPROGRESS t) - (* Select a subset of the goals *) - let tclSELECT = let open Goal_select in function - | SelectNth i -> Proofview.tclFOCUS i i - | SelectList l -> Proofview.tclFOCUSLIST l - | SelectId id -> Proofview.tclFOCUSID id - | SelectAll -> anomaly ~label:"tclSELECT" Pp.(str "SelectAll not allowed here") - | SelectAlreadyFocused -> - anomaly ~label:"tclSELECT" Pp.(str "SelectAlreadyFocused not allowed here") - (* Check that holes in arguments have been resolved *) let check_evars env sigma extsigma origsigma = @@ -905,4 +896,6 @@ module New = struct let (sigma, t) = Typing.type_of ?refresh env sigma c in Proofview.Unsafe.tclEVARS sigma <*> tac sigma t) + let tclSELECT = Goal_select.tclSELECT + end diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli index 19d08dcc36..c09d268c40 100644 --- a/tactics/tacticals.mli +++ b/tactics/tacticals.mli @@ -206,7 +206,6 @@ module New : sig val tclCOMPLETE : 'a tactic -> 'a tactic val tclSOLVE : unit tactic list -> unit tactic val tclPROGRESS : unit tactic -> unit tactic - val tclSELECT : Goal_select.t -> 'a tactic -> 'a tactic val tclWITHHOLES : bool -> 'a tactic -> Evd.evar_map -> 'a tactic val tclDELAYEDWITHHOLES : bool -> 'a delayed_open -> ('a -> unit tactic) -> unit tactic val tclMAPDELAYEDWITHHOLES : bool -> 'a delayed_open list -> ('a -> unit tactic) -> unit tactic @@ -250,4 +249,7 @@ module New : sig val pf_constr_of_global : GlobRef.t -> constr Proofview.tactic val tclTYPEOFTHEN : ?refresh:bool -> constr -> (evar_map -> types -> unit Proofview.tactic) -> unit Proofview.tactic + + val tclSELECT : ?nosuchgoal:'a tactic -> Goal_select.t -> 'a tactic -> 'a tactic + [@@ocaml.deprecated "Use [Goal_select.tclSELECT]"] end diff --git a/test-suite/ltac2/evar.v b/test-suite/ltac2/evar.v new file mode 100644 index 0000000000..2c82673edd --- /dev/null +++ b/test-suite/ltac2/evar.v @@ -0,0 +1,17 @@ +Require Import Ltac2.Ltac2. + +Goal exists (a: nat), a = 1. +Proof. + match! goal with + | [ |- ?g ] => Control.assert_false (Constr.has_evar g) + end. + eexists. + match! goal with + | [ |- ?g ] => Control.assert_true (Constr.has_evar g) + end. + match! goal with + | [ |- ?x = ?y ] => + Control.assert_true (Constr.is_evar x); + Control.assert_false (Constr.is_evar y) + end. +Abort. diff --git a/test-suite/ltac2/rebind.v b/test-suite/ltac2/rebind.v index 7b3a460c8c..9108871e28 100644 --- a/test-suite/ltac2/rebind.v +++ b/test-suite/ltac2/rebind.v @@ -26,12 +26,10 @@ Ltac2 rec nat_eq n m := | S n => match m with | O => false | S m => nat_eq n m end end. -Ltac2 Type exn ::= [ Assertion_failed ]. - Ltac2 assert_eq n m := match nat_eq n m with | true => () - | false => Control.throw Assertion_failed end. + | false => Control.throw Assertion_failure end. Ltac2 mutable x := O. Ltac2 y := x. diff --git a/test-suite/ltac2/syntax_cast.v b/test-suite/ltac2/syntax_cast.v new file mode 100644 index 0000000000..f62d49173d --- /dev/null +++ b/test-suite/ltac2/syntax_cast.v @@ -0,0 +1,14 @@ +Require Import Ltac2.Ltac2. + +Ltac2 foo0 x y : unit := (). +Ltac2 foo1 : unit := (). +Fail Ltac2 foo2 : unit -> unit := (). +Ltac2 foo3 : unit -> unit := fun (_ : unit) => (). + +Ltac2 bar0 := fun x y : unit => (). +Fail Ltac2 bar1 := fun x : unit => 0. +Ltac2 bar2 := fun x : unit list => []. + +Ltac2 qux0 := let x : unit := () in (). +Ltac2 qux1 () := let x y z : unit := () in x 0 "". +Fail Ltac2 qux2 := let x : unit -> unit := () in (). diff --git a/test-suite/output/ltac2_deprecated.out b/test-suite/output/ltac2_deprecated.out new file mode 100644 index 0000000000..d17b719bcd --- /dev/null +++ b/test-suite/output/ltac2_deprecated.out @@ -0,0 +1,12 @@ +File "stdin", line 13, characters 11-14: +Warning: Ltac2 definition foo is deprecated. test_definition +[deprecated-ltac2-definition,deprecated] +- : unit = () +File "stdin", line 14, characters 11-14: +Warning: Ltac2 alias bar is deprecated. test_notation +[deprecated-ltac2-alias,deprecated] +- : unit = () +File "stdin", line 15, characters 11-14: +Warning: Ltac2 definition qux is deprecated. test_external +[deprecated-ltac2-definition,deprecated] +- : 'a array -> int = <fun> diff --git a/test-suite/output/ltac2_deprecated.v b/test-suite/output/ltac2_deprecated.v new file mode 100644 index 0000000000..9598a5979c --- /dev/null +++ b/test-suite/output/ltac2_deprecated.v @@ -0,0 +1,15 @@ +Require Import Ltac2.Ltac2. + +#[deprecated(note="test_definition")] +Ltac2 foo := (). + +#[deprecated(note="test_notation")] +Ltac2 Notation bar := (). + +#[deprecated(note="test_external")] +Ltac2 @ external qux : 'a array -> int := "ltac2" "array_length". +(* Randomly picked external function *) + +Ltac2 Eval foo. +Ltac2 Eval bar. +Ltac2 Eval qux. diff --git a/user-contrib/Ltac2/Constr.v b/user-contrib/Ltac2/Constr.v index 72cac900cd..fa056910b8 100644 --- a/user-contrib/Ltac2/Constr.v +++ b/user-contrib/Ltac2/Constr.v @@ -96,3 +96,54 @@ Ltac2 @ external in_context : ident -> constr -> (unit -> unit) -> constr := "lt Ltac2 @ external pretype : preterm -> constr := "ltac2" "constr_pretype". (** Pretype the provided preterm. Assumes the goal to be focussed. *) + + +Ltac2 is_evar(c: constr) := + match Unsafe.kind c with + | Unsafe.Evar _ _ => true + | _ => false + end. + +Ltac2 @ external has_evar : constr -> bool := "ltac2" "constr_has_evar". + +Ltac2 is_var(c: constr) := + match Unsafe.kind c with + | Unsafe.Var _ => true + | _ => false + end. + +Ltac2 is_fix(c: constr) := + match Unsafe.kind c with + | Unsafe.Fix _ _ _ _ => true + | _ => false + end. + +Ltac2 is_cofix(c: constr) := + match Unsafe.kind c with + | Unsafe.CoFix _ _ _ => true + | _ => false + end. + +Ltac2 is_ind(c: constr) := + match Unsafe.kind c with + | Unsafe.Ind _ _ => true + | _ => false + end. + +Ltac2 is_constructor(c: constr) := + match Unsafe.kind c with + | Unsafe.Constructor _ _ => true + | _ => false + end. + +Ltac2 is_proj(c: constr) := + match Unsafe.kind c with + | Unsafe.Proj _ _ => true + | _ => false + end. + +Ltac2 is_const(c: constr) := + match Unsafe.kind c with + | Unsafe.Constant _ _ => true + | _ => false + end. diff --git a/user-contrib/Ltac2/Control.v b/user-contrib/Ltac2/Control.v index 8b9d53a433..31c8871ff8 100644 --- a/user-contrib/Ltac2/Control.v +++ b/user-contrib/Ltac2/Control.v @@ -98,6 +98,12 @@ Ltac2 assert_bounds (msg : string) (test : bool) := | false => throw_out_of_bounds msg end. +Ltac2 assert_true b := + if b then () else throw Assertion_failure. + +Ltac2 assert_false b := + if b then throw Assertion_failure else (). + (** Short form backtracks *) Ltac2 backtrack_tactic_failure (msg : string) := diff --git a/user-contrib/Ltac2/Init.v b/user-contrib/Ltac2/Init.v index 097a0ca25f..19c89d7266 100644 --- a/user-contrib/Ltac2/Init.v +++ b/user-contrib/Ltac2/Init.v @@ -80,3 +80,6 @@ Ltac2 Type exn ::= [ Invalid_argument (message option) ]. Ltac2 Type exn ::= [ Tactic_failure (message option) ]. (** Generic error for tactic failure. *) + +Ltac2 Type exn ::= [ Assertion_failure ]. +(** Used to indicate that an Ltac2 function ran into a situation that should never occcur. *) diff --git a/user-contrib/Ltac2/g_ltac2.mlg b/user-contrib/Ltac2/g_ltac2.mlg index 548e12d611..4ef5c1a918 100644 --- a/user-contrib/Ltac2/g_ltac2.mlg +++ b/user-contrib/Ltac2/g_ltac2.mlg @@ -99,6 +99,15 @@ let pattern_of_qualid qid = else CErrors.user_err ?loc:qid.CAst.loc (Pp.str "Syntax error") +let opt_fun ?loc args ty e = + let e = match ty with + | None -> e + | Some ty -> CAst.make ?loc:e.CAst.loc (CTacCnv (e, ty)) + in + match args with + | [] -> e + | _ :: _ -> CAst.make ?loc (CTacFun (args, e)) + } GRAMMAR EXTEND Gram @@ -138,8 +147,8 @@ GRAMMAR EXTEND Gram [ "6" RIGHTA [ e1 = SELF; ";"; e2 = SELF -> { CAst.make ~loc @@ CTacSeq (e1, e2) } ] | "5" - [ "fun"; it = LIST1 input_fun ; "=>"; body = ltac2_expr LEVEL "6" -> - { CAst.make ~loc @@ CTacFun (it, body) } + [ "fun"; it = LIST1 input_fun; ty = type_cast; "=>"; body = ltac2_expr LEVEL "6" -> + { opt_fun ~loc it ty body } | "let"; isrec = rec_flag; lc = LIST1 let_clause SEP "with"; "in"; e = ltac2_expr LEVEL "6" -> @@ -236,22 +245,24 @@ GRAMMAR EXTEND Gram | tac = ltac2_expr -> { [], tac } ] ] ; + type_cast: + [ [ -> { None } + | ":"; ty = ltac2_type -> { Some ty } + ] ] + ; let_clause: - [ [ binder = let_binder; ":="; te = ltac2_expr -> + [ [ binder = let_binder; ty = type_cast; ":="; te = ltac2_expr -> { let (pat, fn) = binder in - let te = match fn with - | None -> te - | Some args -> CAst.make ~loc @@ CTacFun (args, te) - in + let te = opt_fun ~loc fn ty te in (pat, te) } ] ] ; let_binder: [ [ pats = LIST1 input_fun -> { match pats with - | [{CAst.v=CPatVar _} as pat] -> (pat, None) - | ({CAst.v=CPatVar (Name id)} as pat) :: args -> (pat, Some args) - | [pat] -> (pat, None) + | [{CAst.v=CPatVar _} as pat] -> (pat, []) + | ({CAst.v=CPatVar (Name id)} as pat) :: args -> (pat, args) + | [pat] -> (pat, []) | _ -> CErrors.user_err ~loc (str "Invalid pattern") } ] ] ; @@ -287,9 +298,8 @@ GRAMMAR EXTEND Gram [ [ b = tac2pat LEVEL "0" -> { b } ] ] ; tac2def_body: - [ [ name = binder; it = LIST0 input_fun; ":="; e = ltac2_expr -> - { let e = if List.is_empty it then e else CAst.make ~loc @@ CTacFun (it, e) in - (name, e) } + [ [ name = binder; it = LIST0 input_fun; ty = type_cast; ":="; e = ltac2_expr -> + { (name, opt_fun ~loc it ty e) } ] ] ; tac2def_val: @@ -905,8 +915,8 @@ let classify_ltac2 = function } VERNAC COMMAND EXTEND VernacDeclareTactic2Definition -| #[ local = locality ] [ "Ltac2" ltac2_entry(e) ] => { classify_ltac2 e } -> { - Tac2entries.register_struct ?local e +| #[ deprecation = deprecation; local = locality ] [ "Ltac2" ltac2_entry(e) ] => { classify_ltac2 e } -> { + Tac2entries.register_struct ?deprecation ?local e } | ![proof_opt_query] [ "Ltac2" "Eval" ltac2_expr(e) ] => { Vernacextend.classify_as_sideeff } -> { fun ~pstate -> Tac2entries.perform_eval ~pstate e diff --git a/user-contrib/Ltac2/tac2core.ml b/user-contrib/Ltac2/tac2core.ml index bcf9ece7c8..fa7df5dfeb 100644 --- a/user-contrib/Ltac2/tac2core.ml +++ b/user-contrib/Ltac2/tac2core.ml @@ -755,6 +755,12 @@ let () = define1 "constr_binder_type" (repr_ext val_binder) begin fun (bnd, ty) return (of_constr ty) end +let () = define1 "constr_has_evar" constr begin fun c -> + Proofview.tclEVARMAP >>= fun sigma -> + let b = Evarutil.has_undefined_evars sigma c in + Proofview.tclUNIT (Value.of_bool b) +end + (** Patterns *) let empty_context = EConstr.mkMeta Constr_matching.special_meta diff --git a/user-contrib/Ltac2/tac2entries.ml b/user-contrib/Ltac2/tac2entries.ml index faa1e74728..d2e74609a2 100644 --- a/user-contrib/Ltac2/tac2entries.ml +++ b/user-contrib/Ltac2/tac2entries.ml @@ -57,6 +57,7 @@ type tacdef = { tacdef_mutable : bool; tacdef_expr : glb_tacexpr; tacdef_type : type_scheme; + tacdef_deprecation : Deprecation.t option; } let perform_tacdef visibility ((sp, kn), def) = @@ -65,6 +66,7 @@ let perform_tacdef visibility ((sp, kn), def) = Tac2env.gdata_expr = def.tacdef_expr; gdata_type = def.tacdef_type; gdata_mutable = def.tacdef_mutable; + gdata_deprecation = def.tacdef_deprecation; } in Tac2env.define_global kn data @@ -77,6 +79,7 @@ let cache_tacdef ((sp, kn), def) = Tac2env.gdata_expr = def.tacdef_expr; gdata_type = def.tacdef_type; gdata_mutable = def.tacdef_mutable; + gdata_deprecation = def.tacdef_deprecation; } in Tac2env.define_global kn data @@ -322,7 +325,7 @@ let check_lowercase {loc;v=id} = if Tac2env.is_constructor (Libnames.qualid_of_ident id) then user_err ?loc (str "The identifier " ++ Id.print id ++ str " must be lowercase") -let register_ltac ?(local = false) ?(mut = false) isrec tactics = +let register_ltac ?deprecation ?(local = false) ?(mut = false) isrec tactics = let map ({loc;v=na}, e) = let id = match na with | Anonymous -> @@ -359,6 +362,7 @@ let register_ltac ?(local = false) ?(mut = false) isrec tactics = tacdef_mutable = mut; tacdef_expr = e; tacdef_type = t; + tacdef_deprecation = deprecation; } in ignore (Lib.add_leaf id (inTacDef def)) in @@ -453,7 +457,7 @@ let register_typedef ?(local = false) isrec types = let iter (id, def) = ignore (Lib.add_leaf id (inTypDef def)) in List.iter iter types -let register_primitive ?(local = false) {loc;v=id} t ml = +let register_primitive ?deprecation ?(local = false) {loc;v=id} t ml = let t = intern_open_type t in let rec count_arrow = function | GTypArrow (_, t) -> 1 + count_arrow t @@ -477,6 +481,7 @@ let register_primitive ?(local = false) {loc;v=id} t ml = tacdef_mutable = false; tacdef_expr = e; tacdef_type = t; + tacdef_deprecation = deprecation; } in ignore (Lib.add_leaf id (inTacDef def)) @@ -599,6 +604,18 @@ let parse_token = function let loc = loc_of_token tok in CErrors.user_err ?loc (str "Invalid parsing token") +let rec print_scope = function +| SexprStr s -> str s.CAst.v +| SexprInt i -> int i.CAst.v +| SexprRec (_, {v=na}, []) -> Option.cata Id.print (str "_") na +| SexprRec (_, {v=na}, e) -> + Option.cata Id.print (str "_") na ++ str "(" ++ pr_sequence print_scope e ++ str ")" + +let print_token = function +| SexprStr {v=s} -> quote (str s) +| SexprRec (_, {v=na}, [tok]) -> print_scope tok +| _ -> assert false + end let parse_scope = ParseToken.parse_scope @@ -608,6 +625,7 @@ type synext = { synext_exp : raw_tacexpr; synext_lev : int option; synext_loc : bool; + synext_depr : Deprecation.t option; } type krule = @@ -628,10 +646,20 @@ let rec get_rule (tok : scope_rule token list) : krule = match tok with let act k _ = act k in KRule (rule, act) +let deprecated_ltac2_notation = + Deprecation.create_warning + ~object_name:"Ltac2 notation" + ~warning_name:"deprecated-ltac2-notation" + (fun (toks : sexpr list) -> pr_sequence ParseToken.print_token toks) + let perform_notation syn st = let tok = List.rev_map ParseToken.parse_token syn.synext_tok in let KRule (rule, act) = get_rule tok in let mk loc args = + let () = match syn.synext_depr with + | None -> () + | Some depr -> deprecated_ltac2_notation ~loc (syn.synext_tok, depr) + in let map (na, e) = ((CAst.make ?loc:e.loc @@ CPatVar na), e) in @@ -671,23 +699,24 @@ let inTac2Notation : synext -> obj = type abbreviation = { abbr_body : raw_tacexpr; + abbr_depr : Deprecation.t option; } let perform_abbreviation visibility ((sp, kn), abbr) = let () = Tac2env.push_ltac visibility sp (TacAlias kn) in - Tac2env.define_alias kn abbr.abbr_body + Tac2env.define_alias ?deprecation:abbr.abbr_depr kn abbr.abbr_body let load_abbreviation i obj = perform_abbreviation (Until i) obj let open_abbreviation i obj = perform_abbreviation (Exactly i) obj let cache_abbreviation ((sp, kn), abbr) = let () = Tac2env.push_ltac (Until 1) sp (TacAlias kn) in - Tac2env.define_alias kn abbr.abbr_body + Tac2env.define_alias ?deprecation:abbr.abbr_depr kn abbr.abbr_body let subst_abbreviation (subst, abbr) = let body' = subst_rawexpr subst abbr.abbr_body in if body' == abbr.abbr_body then abbr - else { abbr_body = body' } + else { abbr_body = body'; abbr_depr = abbr.abbr_depr } let classify_abbreviation o = Substitute o @@ -699,12 +728,12 @@ let inTac2Abbreviation : abbreviation -> obj = subst_function = subst_abbreviation; classify_function = classify_abbreviation} -let register_notation ?(local = false) tkn lev body = match tkn, lev with +let register_notation ?deprecation ?(local = false) tkn lev body = match tkn, lev with | [SexprRec (_, {loc;v=Some id}, [])], None -> (* Tactic abbreviation *) let () = check_lowercase CAst.(make ?loc id) in let body = Tac2intern.globalize Id.Set.empty body in - let abbr = { abbr_body = body } in + let abbr = { abbr_body = body; abbr_depr = deprecation } in ignore (Lib.add_leaf id (inTac2Abbreviation abbr)) | _ -> (* Check that the tokens make sense *) @@ -723,6 +752,7 @@ let register_notation ?(local = false) tkn lev body = match tkn, lev with synext_exp = body; synext_lev = lev; synext_loc = local; + synext_depr = deprecation; } in Lib.add_anonymous_leaf (inTac2Notation ext) @@ -811,24 +841,11 @@ let perform_eval ~pstate e = Goal_select.get_default_goal_selector (), Declare.Proof.get pstate in - let v = match selector with - | Goal_select.SelectNth i -> Proofview.tclFOCUS i i v - | Goal_select.SelectList l -> Proofview.tclFOCUSLIST l v - | Goal_select.SelectId id -> Proofview.tclFOCUSID id v - | Goal_select.SelectAll -> v - | Goal_select.SelectAlreadyFocused -> - let open Proofview.Notations in - Proofview.numgoals >>= fun n -> - if Int.equal n 1 then v - else - let e = CErrors.UserError - (None, - Pp.(str "Expected a single focused goal but " ++ - int n ++ str " goals are focused.")) - in - let info = Exninfo.reify () in - Proofview.tclZERO ~info e + let nosuchgoal = + let info = Exninfo.reify () in + Proofview.tclZERO ~info (Proof.SuggestNoSuchGoals (1,proof)) in + let v = Goal_select.tclSELECT ~nosuchgoal selector v in let (proof, _, ans) = Proof.run_tactic (Global.env ()) v proof in let { Proof.sigma } = Proof.data proof in let name = int_name () in @@ -838,12 +855,21 @@ let perform_eval ~pstate e = (** Toplevel entries *) -let register_struct ?local str = match str with -| StrVal (mut, isrec, e) -> register_ltac ?local ~mut isrec e -| StrTyp (isrec, t) -> register_type ?local isrec t -| StrPrm (id, t, ml) -> register_primitive ?local id t ml -| StrSyn (tok, lev, e) -> register_notation ?local tok lev e -| StrMut (qid, old, e) -> register_redefinition ?local qid old e +let unsupported_deprecation = function +| None -> () +| Some _ -> + Attributes.unsupported_attributes ["deprecated", Attributes.VernacFlagEmpty] + +let register_struct ?deprecation ?local str = match str with +| StrVal (mut, isrec, e) -> register_ltac ?deprecation ?local ~mut isrec e +| StrTyp (isrec, t) -> + let () = unsupported_deprecation deprecation in (* TODO *) + register_type ?local isrec t +| StrPrm (id, t, ml) -> register_primitive ?deprecation ?local id t ml +| StrSyn (tok, lev, e) -> register_notation ?deprecation ?local tok lev e +| StrMut (qid, old, e) -> + let () = unsupported_deprecation deprecation in (* TODO: what does that mean? *) + register_redefinition ?local qid old e (** Toplevel exception *) diff --git a/user-contrib/Ltac2/tac2entries.mli b/user-contrib/Ltac2/tac2entries.mli index 782968c6e1..a1e13b60fe 100644 --- a/user-contrib/Ltac2/tac2entries.mli +++ b/user-contrib/Ltac2/tac2entries.mli @@ -14,22 +14,19 @@ open Tac2expr (** {5 Toplevel definitions} *) -val register_ltac : ?local:bool -> ?mut:bool -> rec_flag -> +val register_ltac : ?deprecation:Deprecation.t -> ?local:bool -> ?mut:bool -> rec_flag -> (Names.lname * raw_tacexpr) list -> unit val register_type : ?local:bool -> rec_flag -> (qualid * redef_flag * raw_quant_typedef) list -> unit -val register_primitive : ?local:bool -> +val register_primitive : ?deprecation:Deprecation.t -> ?local:bool -> Names.lident -> raw_typexpr -> ml_tactic_name -> unit -val register_struct - : ?local:bool - -> strexpr - -> unit +val register_struct : ?deprecation:Deprecation.t -> ?local:bool -> strexpr -> unit -val register_notation : ?local:bool -> sexpr list -> int option -> - raw_tacexpr -> unit +val register_notation : ?deprecation:Deprecation.t -> ?local:bool -> sexpr list -> + int option -> raw_tacexpr -> unit val perform_eval : pstate:Declare.Proof.t option -> raw_tacexpr -> unit diff --git a/user-contrib/Ltac2/tac2env.ml b/user-contrib/Ltac2/tac2env.ml index 5479ba0d54..5eb57c8f9b 100644 --- a/user-contrib/Ltac2/tac2env.ml +++ b/user-contrib/Ltac2/tac2env.ml @@ -18,6 +18,7 @@ type global_data = { gdata_expr : glb_tacexpr; gdata_type : type_scheme; gdata_mutable : bool; + gdata_deprecation : Deprecation.t option; } type constructor_data = { @@ -35,12 +36,17 @@ type projection_data = { pdata_indx : int; } +type alias_data = { + alias_body : raw_tacexpr; + alias_depr : Deprecation.t option; +} + type ltac_state = { ltac_tactics : global_data KNmap.t; ltac_constructors : constructor_data KNmap.t; ltac_projections : projection_data KNmap.t; ltac_types : glb_quant_typedef KNmap.t; - ltac_aliases : raw_tacexpr KNmap.t; + ltac_aliases : alias_data KNmap.t; } let empty_state = { @@ -79,9 +85,10 @@ let define_type kn e = let interp_type kn = KNmap.find kn ltac_state.contents.ltac_types -let define_alias kn tac = +let define_alias ?deprecation kn tac = let state = !ltac_state in - ltac_state := { state with ltac_aliases = KNmap.add kn tac state.ltac_aliases } + let data = { alias_body = tac; alias_depr = deprecation } in + ltac_state := { state with ltac_aliases = KNmap.add kn data state.ltac_aliases } let interp_alias kn = KNmap.find kn ltac_state.contents.ltac_aliases diff --git a/user-contrib/Ltac2/tac2env.mli b/user-contrib/Ltac2/tac2env.mli index 95dcdd7e1b..3800ad0198 100644 --- a/user-contrib/Ltac2/tac2env.mli +++ b/user-contrib/Ltac2/tac2env.mli @@ -23,6 +23,7 @@ type global_data = { gdata_expr : glb_tacexpr; gdata_type : type_scheme; gdata_mutable : bool; + gdata_deprecation : Deprecation.t option; } val define_global : ltac_constant -> global_data -> unit @@ -72,8 +73,13 @@ val interp_projection : ltac_projection -> projection_data (** {5 Toplevel definition of aliases} *) -val define_alias : ltac_constant -> raw_tacexpr -> unit -val interp_alias : ltac_constant -> raw_tacexpr +type alias_data = { + alias_body : raw_tacexpr; + alias_depr : Deprecation.t option; +} + +val define_alias : ?deprecation:Deprecation.t -> ltac_constant -> raw_tacexpr -> unit +val interp_alias : ltac_constant -> alias_data (** {5 Name management} *) diff --git a/user-contrib/Ltac2/tac2intern.ml b/user-contrib/Ltac2/tac2intern.ml index ddf70a5a65..90c8528203 100644 --- a/user-contrib/Ltac2/tac2intern.ml +++ b/user-contrib/Ltac2/tac2intern.ml @@ -655,6 +655,35 @@ let is_alias env qid = match get_variable env qid with | ArgArg (TacAlias _) -> true | ArgVar _ | (ArgArg (TacConstant _)) -> false +let is_user_name qid = match qid with +| AbsKn _ -> false +| RelId _ -> true + +let deprecated_ltac2_alias = + Deprecation.create_warning + ~object_name:"Ltac2 alias" + ~warning_name:"deprecated-ltac2-alias" + (fun kn -> pr_qualid (Tac2env.shortest_qualid_of_ltac (TacAlias kn))) + +let deprecated_ltac2_def = + Deprecation.create_warning + ~object_name:"Ltac2 definition" + ~warning_name:"deprecated-ltac2-definition" + (fun kn -> pr_qualid (Tac2env.shortest_qualid_of_ltac (TacConstant kn))) + +let check_deprecated_ltac2 ?loc qid def = + if is_user_name qid then match def with + | TacAlias kn -> + begin match (Tac2env.interp_alias kn).alias_depr with + | None -> () + | Some depr -> deprecated_ltac2_alias ?loc (kn, depr) + end + | TacConstant kn -> + begin match (Tac2env.interp_global kn).gdata_deprecation with + | None -> () + | Some depr -> deprecated_ltac2_def ?loc (kn, depr) + end + let rec intern_rec env {loc;v=e} = match e with | CTacAtm atm -> intern_atm env atm | CTacRef qid -> @@ -663,11 +692,12 @@ let rec intern_rec env {loc;v=e} = match e with let sch = Id.Map.find id env.env_var in (GTacVar id, fresh_mix_type_scheme env sch) | ArgArg (TacConstant kn) -> - let { Tac2env.gdata_type = sch } = + let { Tac2env.gdata_type = sch; gdata_deprecation = depr } = try Tac2env.interp_global kn with Not_found -> CErrors.anomaly (str "Missing hardwired primitive " ++ KerName.print kn) in + let () = check_deprecated_ltac2 ?loc qid (TacConstant kn) in (GTacRef kn, fresh_type_scheme env sch) | ArgArg (TacAlias kn) -> let e = @@ -675,7 +705,8 @@ let rec intern_rec env {loc;v=e} = match e with with Not_found -> CErrors.anomaly (str "Missing hardwired alias " ++ KerName.print kn) in - intern_rec env e + let () = check_deprecated_ltac2 ?loc qid (TacAlias kn) in + intern_rec env e.alias_body end | CTacCst qid -> let kn = get_constructor env qid in @@ -695,12 +726,13 @@ let rec intern_rec env {loc;v=e} = match e with | CTacApp ({loc;v=CTacCst qid}, args) -> let kn = get_constructor env qid in intern_constructor env loc kn args -| CTacApp ({v=CTacRef qid}, args) when is_alias env qid -> +| CTacApp ({v=CTacRef qid; loc=aloc}, args) when is_alias env qid -> let kn = match get_variable env qid with | ArgArg (TacAlias kn) -> kn | ArgVar _ | (ArgArg (TacConstant _)) -> assert false in let e = Tac2env.interp_alias kn in + let () = check_deprecated_ltac2 ?loc:aloc qid (TacAlias kn) in let map arg = (* Thunk alias arguments *) let loc = arg.loc in @@ -709,7 +741,7 @@ let rec intern_rec env {loc;v=e} = match e with CAst.make ?loc @@ CTacFun ([var], arg) in let args = List.map map args in - intern_rec env (CAst.make ?loc @@ CTacApp (e, args)) + intern_rec env (CAst.make ?loc @@ CTacApp (e.alias_body, args)) | CTacApp (f, args) -> let loc = f.loc in let (f, ft) = intern_rec env f in @@ -1243,7 +1275,9 @@ let rec globalize ids ({loc;v=er} as e) = match er with let mem id = Id.Set.mem id ids in begin match get_variable0 mem ref with | ArgVar _ -> e - | ArgArg kn -> CAst.make ?loc @@ CTacRef (AbsKn kn) + | ArgArg kn -> + let () = check_deprecated_ltac2 ?loc ref kn in + CAst.make ?loc @@ CTacRef (AbsKn kn) end | CTacCst qid -> let knc = get_constructor () qid in |