diff options
38 files changed, 224 insertions, 207 deletions
diff --git a/doc/changelog/04-tactics/09288-injection-as.rst b/doc/changelog/04-tactics/09288-injection-as.rst new file mode 100644 index 0000000000..6a74551f06 --- /dev/null +++ b/doc/changelog/04-tactics/09288-injection-as.rst @@ -0,0 +1,4 @@ +- Documented syntax :n:`injection @term as [= {+ @intropattern} ]` as + an alternative to :n:`injection @term as {+ @simple_intropattern}` using + the standard :n:`@injection_intropattern` syntax (`#09288 + <https://github.com/coq/coq/pull/09288>`_, by Hugo Herbelin). diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst index 3149d64d3e..cc4976587d 100644 --- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst +++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst @@ -455,7 +455,7 @@ the latter can be replaced by the open syntax ``of term`` or following extension of the binder syntax: .. prodn:: - binder += & @term | of @term + binder += {| & @term | of @term } Caveat: ``& T`` and ``of T`` abbreviations have to appear at the end of a binder list. For instance, the usual two-constructor polymorphic @@ -1340,7 +1340,7 @@ The general syntax of the discharging tactical ``:`` is: :undocumented: .. prodn:: - d_item ::= {? @occ_switch %| @clear_switch } @term + d_item ::= {? {| @occ_switch | @clear_switch } } @term .. prodn:: clear_switch ::= { {+ @ident } } @@ -1556,19 +1556,19 @@ whose general syntax is :undocumented: .. prodn:: - i_item ::= @i_pattern %| @s_item %| @clear_switch %| @i_view %| @i_block + i_item ::= {| @i_pattern | @s_item | @clear_switch | @i_view | @i_block } .. prodn:: - s_item ::= /= %| // %| //= + s_item ::= {| /= | // | //= } .. prodn:: - i_view ::= {? %{%} } /@term %| /ltac:( @tactic ) + i_view ::= {? %{%} } {| /@term | /ltac:( @tactic ) } .. prodn:: - i_pattern ::= @ident %| > %| _ %| ? %| * %| + %| {? @occ_switch } -> %| {? @occ_switch }<- %| [ {?| @i_item } ] %| - %| [: {+ @ident } ] + i_pattern ::= {| @ident | > | _ | ? | * | + | {? @occ_switch } {| -> | <- } | [ {?| @i_item } ] | - | [: {+ @ident } ] } .. prodn:: - i_block ::= [^ @ident ] %| [^~ @ident ] %| [^~ @num ] + i_block ::= {| [^ @ident ] | [^~ {| @ident | @num } ] } The ``=>`` tactical first executes :token:`tactic`, then the :token:`i_item`\s, left to right. An :token:`s_item` specifies a @@ -2390,7 +2390,7 @@ of a local definition during the generalization phase, the name of the local definition must be written between parentheses, like in ``rewrite H in H1 (def_n) H2.`` -.. tacv:: @tactic in {+ @clear_switch | {? @ } @ident | ( @ident ) | ( {? @ } @ident := @c_pattern ) } {? * } +.. tacv:: @tactic in {+ {| @clear_switch | {? @}@ident | ( @ident ) | ( {? @}@ident := @c_pattern ) } } {? * } This is the most general form of the ``in`` tactical. In its simplest form the last option lets one rename hypotheses that @@ -2492,7 +2492,7 @@ tactic: The behavior of the defective have tactic makes it possible to generalize it in the following general construction: -.. tacn:: have {* @i_item } {? @i_pattern } {? @s_item | {+ @ssr_binder } } {? : @term } {? := @term | by @tactic } +.. tacn:: have {* @i_item } {? @i_pattern } {? {| @s_item | {+ @ssr_binder } } } {? : @term } {? {| := @term | by @tactic } } :undocumented: Open syntax is supported for both :token:`term`. For the description @@ -2920,7 +2920,7 @@ Advanced generalization The complete syntax for the items on the left hand side of the ``/`` separator is the following one: -.. tacv:: wlog … : {? @clear_switch | {? @ } @ident | ( {? @ } @ident := @c_pattern) } / @term +.. tacv:: wlog … : {? {| @clear_switch | {? @}@ident | ( {? @}@ident := @c_pattern) } } / @term :undocumented: Clear operations are intertwined with generalization operations. This @@ -3020,13 +3020,13 @@ A rewrite step :token:`rstep` has the general form: rstep ::= {? @r_prefix } @r_item .. prodn:: - r_prefix ::= {? - } {? @mult } {? @occ_switch %| @clear_switch } {? [ @r_pattern ] } + r_prefix ::= {? - } {? @mult } {? {| @occ_switch | @clear_switch } } {? [ @r_pattern ] } .. prodn:: - r_pattern ::= @term %| in {? @ident in } @term %| %( @term in %| @term as %) @ident in @term + r_pattern ::= {| @term | in {? @ident in } @term | {| @term in | @term as } @ident in @term } .. prodn:: - r_item ::= {? / } @term %| @s_item + r_item ::= {| {? / } @term | @s_item } An :token:`r_prefix` contains annotations to qualify where and how the rewrite operation should be performed: @@ -3702,7 +3702,7 @@ The under tactic The convenience :tacn:`under` tactic supports the following syntax: -.. tacn:: under {? @r_prefix } @term {? => {+ @i_item}} {? do ( @tactic | [ {*| @tactic } ] ) } +.. tacn:: under {? @r_prefix } @term {? => {+ @i_item}} {? do {| @tactic | [ {*| @tactic } ] } } :name: under Operate under the context proved to be extensional by @@ -5167,7 +5167,7 @@ Interpreting assumptions The general form of an assumption view tactic is: -.. tacv:: [move | case] / @term +.. tacv:: {| move | case } / @term :undocumented: The term , called the *view lemma* can be: @@ -5514,7 +5514,7 @@ Parameters |SSR| tactics .. prodn:: - d_tactic ::= elim %| case %| congr %| apply %| exact %| move + d_tactic ::= {| elim | case | congr | apply | exact | move } Notation scope @@ -5526,7 +5526,7 @@ Module name Natural number -.. prodn:: natural ::= @num %| @ident +.. prodn:: natural ::= {| @num | @ident } where :token:`ident` is an Ltac variable denoting a standard |Coq| numeral (should not be the name of a tactic which can be followed by a @@ -5535,7 +5535,7 @@ bracket ``[``, like ``do``, ``have``,…) Items and switches ~~~~~~~~~~~~~~~~~~ -.. prodn:: ssr_binder ::= @ident %| ( @ident {? : @term } ) +.. prodn:: ssr_binder ::= {| @ident | ( @ident {? : @term } ) } binder see :ref:`abbreviations_ssr`. @@ -5543,33 +5543,33 @@ binder see :ref:`abbreviations_ssr`. clear switch see :ref:`discharge_ssr` -.. prodn:: c_pattern ::= {? @term in %| @term as } @ident in @term +.. prodn:: c_pattern ::= {? {| @term in | @term as } } @ident in @term context pattern see :ref:`contextual_patterns_ssr` -.. prodn:: d_item ::= {? @occ_switch %| @clear_switch } {? @term %| ( @c_pattern ) } +.. prodn:: d_item ::= {? {| @occ_switch | @clear_switch } } {? {| @term | ( @c_pattern ) } } discharge item see :ref:`discharge_ssr` -.. prodn:: gen_item ::= {? @ } @ident %| ( @ident ) %| ( {? @ } @ident := @c_pattern ) +.. prodn:: gen_item ::= {| {? @ } @ident | ( @ident ) | ( {? @ } @ident := @c_pattern ) } generalization item see :ref:`structure_ssr` -.. prodn:: i_pattern ::= @ident %| > %| _ %| ? %| * %| + %| {? @occ_switch } -> %| {? @occ_switch } <- %| [ {?| @i_item } ] %| - %| [: {+ @ident } ] +.. prodn:: i_pattern ::= {| @ident | > | _ | ? | * | + | {? @occ_switch } {| -> | <- } | [ {?| @i_item } ] | - | [: {+ @ident } ] } intro pattern :ref:`introduction_ssr` -.. prodn:: i_item ::= @clear_switch %| @s_item %| @i_pattern %| @i_view %| @i_block +.. prodn:: i_item ::= {| @clear_switch | @s_item | @i_pattern | @i_view | @i_block } view :ref:`introduction_ssr` .. prodn:: - i_view ::= {? %{%} } /@term %| /ltac:( @tactic ) + i_view ::= {? %{%} } {| /@term | /ltac:( @tactic ) } intro block :ref:`introduction_ssr` .. prodn:: - i_block ::= [^ @ident ] %| [^~ @ident ] %| [^~ @num ] + i_block ::= {| [^ @ident ] | [^~ {| @ident | @num } ] } intro item see :ref:`introduction_ssr` @@ -5577,7 +5577,7 @@ intro item see :ref:`introduction_ssr` multiplier see :ref:`iteration_ssr` -.. prodn:: occ_switch ::= { {? + %| - } {* @num } } +.. prodn:: occ_switch ::= { {? {| + | - } } {* @num } } occur. switch see :ref:`occurrence_selection_ssr` @@ -5585,19 +5585,19 @@ occur. switch see :ref:`occurrence_selection_ssr` multiplier see :ref:`iteration_ssr` -.. prodn:: mult_mark ::= ? %| ! +.. prodn:: mult_mark ::= {| ? | ! } multiplier mark see :ref:`iteration_ssr` -.. prodn:: r_item ::= {? / } @term %| @s_item +.. prodn:: r_item ::= {| {? / } @term | @s_item } rewrite item see :ref:`rewriting_ssr` -.. prodn:: r_prefix ::= {? - } {? @int_mult } {? @occ_switch %| @clear_switch } {? [ @r_pattern ] } +.. prodn:: r_prefix ::= {? - } {? @int_mult } {? {| @occ_switch | @clear_switch } } {? [ @r_pattern ] } rewrite prefix see :ref:`rewriting_ssr` -.. prodn:: r_pattern ::= @term %| @c_pattern %| in {? @ident in } @term +.. prodn:: r_pattern ::= {| @term | @c_pattern | in {? @ident in } @term } rewrite pattern see :ref:`rewriting_ssr` @@ -5605,7 +5605,7 @@ rewrite pattern see :ref:`rewriting_ssr` rewrite step see :ref:`rewriting_ssr` -.. prodn:: s_item ::= /= %| // %| //= +.. prodn:: s_item ::= {| /= | // | //= } simplify switch see :ref:`introduction_ssr` @@ -5640,7 +5640,7 @@ respectively. rewrite (see :ref:`rewriting_ssr`) -.. tacn:: under {? @r_prefix } @term {? => {+ @i_item}} {? do ( @tactic | [ {*| @tactic } ] )} +.. tacn:: under {? @r_prefix } @term {? => {+ @i_item}} {? do {| @tactic | [ {*| @tactic } ] } } under (see :ref:`under_ssr`) @@ -5648,8 +5648,8 @@ respectively. over (see :ref:`over_ssr`) -.. tacn:: have {* @i_item } {? @i_pattern } {? @s_item %| {+ @ssr_binder } } {? : @term } := @term - have {* @i_item } {? @i_pattern } {? @s_item %| {+ @ssr_binder } } : @term {? by @tactic } +.. tacn:: have {* @i_item } {? @i_pattern } {? {| @s_item | {+ @ssr_binder } } } {? : @term } := @term + have {* @i_item } {? @i_pattern } {? {| @s_item | {+ @ssr_binder } } } : @term {? by @tactic } have suff {? @clear_switch } {? @i_pattern } {? : @term } := @term have suff {? @clear_switch } {? @i_pattern } : @term {? by @tactic } gen have {? @ident , } {? @i_pattern } : {+ @gen_item } / @term {? by @tactic } @@ -5658,7 +5658,7 @@ respectively. forward chaining (see :ref:`structure_ssr`) -.. tacn:: wlog {? suff } {? @i_item } : {* @gen_item %| @clear_switch } / @term +.. tacn:: wlog {? suff } {? @i_item } : {* {| @gen_item | @clear_switch } } / @term specializing (see :ref:`structure_ssr`) @@ -5710,7 +5710,7 @@ discharge :ref:`discharge_ssr` introduction see :ref:`introduction_ssr` -.. prodn:: tactic += @tactic in {+ @gen_item %| @clear_switch } {? * } +.. prodn:: tactic += @tactic in {+ {| @gen_item | @clear_switch } } {? * } localization see :ref:`localization_ssr` diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index 67d32835f5..fa6d62ffa2 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -131,16 +131,17 @@ include :tacn:`assert`, :tacn:`intros` and :tacn:`destruct`. simple_intropattern_closed : `naming_intropattern` : _ : `or_and_intropattern` - : `equality_intropattern` + : `rewriting_intropattern` + : `injection_intropattern` naming_intropattern : `ident` : ? : ?`ident` or_and_intropattern : [ `intropattern_list` | ... | `intropattern_list` ] : ( `simple_intropattern` , ... , `simple_intropattern` ) : ( `simple_intropattern` & ... & `simple_intropattern` ) - equality_intropattern : -> + rewriting_intropattern : -> : <- - : [= `intropattern_list` ] + injection_intropattern : [= `intropattern_list` ] or_and_intropattern_loc : `or_and_intropattern` : `ident` @@ -2285,6 +2286,18 @@ and an explanation of the underlying technique. to the number of new equalities. The original equality is erased if it corresponds to a hypothesis. + .. tacv:: injection @term {? with @bindings_list} as @injection_intropattern + injection @num as @injection_intropattern + injection as @injection_intropattern + einjection @term {? with @bindings_list} as @injection_intropattern + einjection @num as @injection_intropattern + einjection as @injection_intropattern + + These are equivalent to the previous variants but using instead the + syntax :token:`injection_intropattern` which :tacn:`intros` + uses. In particular :n:`as [= {+ @simple_intropattern}]` behaves + the same as :n:`as {+ @simple_intropattern}`. + .. flag:: Structural Injection This option ensure that :n:`injection @term` erases the original hypothesis diff --git a/engine/termops.ml b/engine/termops.ml index fcacb53ac4..05bb42ac61 100644 --- a/engine/termops.ml +++ b/engine/termops.ml @@ -306,9 +306,15 @@ let pr_evar_map_gen with_univs pr_evars env sigma = let pr_evar_list env sigma l = let open Evd in + let pr_restrict ev = + match is_restricted_evar sigma ev with + | None -> mt () + | Some ev' -> str " (restricted to " ++ Evar.print ev' ++ str ")" + in let pr (ev, evi) = h 0 (Evar.print ev ++ str "==" ++ pr_evar_info env sigma evi ++ + pr_restrict ev ++ (if evi.evar_body == Evar_empty then str " {" ++ pr_existential_key sigma ev ++ str "}" else mt ())) diff --git a/plugins/ltac/extratactics.mlg b/plugins/ltac/extratactics.mlg index f5098d2a34..4c186dce09 100644 --- a/plugins/ltac/extratactics.mlg +++ b/plugins/ltac/extratactics.mlg @@ -146,6 +146,23 @@ let discrHyp id = let injection_main with_evars c = elimOnConstrWithHoles (injClause None None) with_evars c +let isInjPat pat = match pat.CAst.v with IntroAction (IntroInjection _) -> Some pat.CAst.loc | _ -> None + +let decode_inj_ipat ?loc = function + (* For the "as [= pat1 ... patn ]" syntax *) + | [{ CAst.v = IntroAction (IntroInjection ipat) }] -> ipat + (* For the "as pat1 ... patn" syntax *) + | ([] | [_]) as ipat -> ipat + | pat1::pat2::_ as ipat -> + (* To be sure that there is no confusion of syntax, we check that no [= ...] occurs + in the non-singleton list of patterns *) + match isInjPat pat1 with + | Some _ -> user_err ?loc:pat2.CAst.loc (str "Unexpected pattern.") + | None -> + match List.map_filter isInjPat ipat with + | loc :: _ -> user_err ?loc (str "Unexpected injection pattern.") + | [] -> ipat + } TACTIC EXTEND injection @@ -158,15 +175,15 @@ TACTIC EXTEND einjection END TACTIC EXTEND injection_as | [ "injection" "as" intropattern_list(ipat)] -> - { injClause None (Some ipat) false None } + { injClause None (Some (decode_inj_ipat ipat)) false None } | [ "injection" destruction_arg(c) "as" intropattern_list(ipat)] -> - { mytclWithHoles (injClause None (Some ipat)) false c } + { mytclWithHoles (injClause None (Some (decode_inj_ipat ipat))) false c } END TACTIC EXTEND einjection_as | [ "einjection" "as" intropattern_list(ipat)] -> - { injClause None (Some ipat) true None } + { injClause None (Some (decode_inj_ipat ipat)) true None } | [ "einjection" destruction_arg(c) "as" intropattern_list(ipat)] -> - { mytclWithHoles (injClause None (Some ipat)) true c } + { mytclWithHoles (injClause None (Some (decode_inj_ipat ipat))) true c } END TACTIC EXTEND simple_injection | [ "simple" "injection" ] -> { simpleInjClause None false None } diff --git a/plugins/ltac/g_rewrite.mlg b/plugins/ltac/g_rewrite.mlg index 12b12bc7b0..2fad1f6b6a 100644 --- a/plugins/ltac/g_rewrite.mlg +++ b/plugins/ltac/g_rewrite.mlg @@ -310,12 +310,6 @@ TACTIC EXTEND setoid_transitivity END VERNAC COMMAND EXTEND PrintRewriteHintDb CLASSIFIED AS QUERY -| ![ proof ] [ "Print" "Rewrite" "HintDb" preident(s) ] -> - { (* This command should not use the proof env, keeping previous - behavior as requested in review. *) - fun ~pstate -> - let sigma, env = Option.cata Pfedit.get_current_context - (let e = Global.env () in Evd.from_env e, e) pstate in - Feedback.msg_notice (Autorewrite.print_rewrite_hintdb env sigma s); - pstate } +| [ "Print" "Rewrite" "HintDb" preident(s) ] -> + { Feedback.msg_notice (Autorewrite.print_rewrite_hintdb s) } END diff --git a/plugins/micromega/EnvRing.v b/plugins/micromega/EnvRing.v index 36ed0210e3..b20f45af3e 100644 --- a/plugins/micromega/EnvRing.v +++ b/plugins/micromega/EnvRing.v @@ -925,7 +925,7 @@ Qed. revert P1. induction LM1 as [|(M2,P2') LM2 IH]; simpl; intros. - discriminate. - assert (H':=PNSubst_ok n P3 M2 P2'). destruct PNSubst. - * injection H as <-. rewrite <- PSubstL1_ok; intuition. + * injection H as [= <-]. rewrite <- PSubstL1_ok; intuition. * now apply IH. Qed. diff --git a/plugins/setoid_ring/InitialRing.v b/plugins/setoid_ring/InitialRing.v index 4886c8b9aa..9be2535a3f 100644 --- a/plugins/setoid_ring/InitialRing.v +++ b/plugins/setoid_ring/InitialRing.v @@ -105,7 +105,7 @@ Section ZMORPHISM. Proof. constructor. destruct c;intros;try discriminate. - injection H as <-. + injection H as [= <-]. simpl. unfold Zeq_bool. rewrite Z.compare_refl. trivial. Qed. diff --git a/plugins/setoid_ring/Ring_polynom.v b/plugins/setoid_ring/Ring_polynom.v index f7cb6b688b..c5d396427b 100644 --- a/plugins/setoid_ring/Ring_polynom.v +++ b/plugins/setoid_ring/Ring_polynom.v @@ -894,7 +894,7 @@ Section MakeRingPol. revert P1. induction LM1 as [|(M2,P2') LM2 IH]; simpl; intros. - discriminate. - assert (H':=PNSubst_ok n P3 M2 P2'). destruct PNSubst. - * injection H as <-. rewrite <- PSubstL1_ok; intuition. + * injection H as [= <-]. rewrite <- PSubstL1_ok; intuition. * now apply IH. Qed. diff --git a/plugins/setoid_ring/g_newring.mlg b/plugins/setoid_ring/g_newring.mlg index 6be556b2ae..5dfead2d7e 100644 --- a/plugins/setoid_ring/g_newring.mlg +++ b/plugins/setoid_ring/g_newring.mlg @@ -13,8 +13,6 @@ open Ltac_plugin open Pp open Util -open Libnames -open Printer open Newring_ast open Newring open Stdarg @@ -85,21 +83,10 @@ END VERNAC COMMAND EXTEND AddSetoidRing CLASSIFIED AS SIDEFF | [ "Add" "Ring" ident(id) ":" constr(t) ring_mods_opt(l) ] -> - { let l = match l with None -> [] | Some l -> l in add_theory id t l } - | ![proof] [ "Print" "Rings" ] => { Vernacextend.classify_as_query } -> { - fun ~pstate -> - Feedback.msg_notice (strbrk "The following ring structures have been declared:"); - Spmap.iter (fun fn fi -> - (* We should use the global env here as this shouldn't contain proof - data, however preserving behavior as requested in review. *) - let sigma, env = Option.cata Pfedit.get_current_context - (let e = Global.env () in Evd.from_env e, e) pstate in - Feedback.msg_notice (hov 2 - (Ppconstr.pr_id (Libnames.basename fn)++spc()++ - str"with carrier "++ pr_constr_env env sigma fi.ring_carrier++spc()++ - str"and equivalence relation "++ pr_constr_env env sigma fi.ring_req)) - ) !from_name; - pstate } + { add_theory id t (Option.default [] l) } + | [ "Print" "Rings" ] => { Vernacextend.classify_as_query } -> { + print_rings () + } END TACTIC EXTEND ring_lookup @@ -135,20 +122,9 @@ END VERNAC COMMAND EXTEND AddSetoidField CLASSIFIED AS SIDEFF | [ "Add" "Field" ident(id) ":" constr(t) field_mods_opt(l) ] -> { let l = match l with None -> [] | Some l -> l in add_field_theory id t l } -| ![proof] [ "Print" "Fields" ] => {Vernacextend.classify_as_query} -> { - fun ~pstate -> - Feedback.msg_notice (strbrk "The following field structures have been declared:"); - Spmap.iter (fun fn fi -> - (* We should use the global env here as this shouldn't - contain proof data. *) - let sigma, env = Option.cata Pfedit.get_current_context - (let e = Global.env () in Evd.from_env e, e) pstate in - Feedback.msg_notice (hov 2 - (Ppconstr.pr_id (Libnames.basename fn)++spc()++ - str"with carrier "++ pr_constr_env env sigma fi.field_carrier++spc()++ - str"and equivalence relation "++ pr_constr_env env sigma fi.field_req)) - ) !field_from_name; - pstate } +| [ "Print" "Fields" ] => {Vernacextend.classify_as_query} -> { + print_fields () + } END TACTIC EXTEND field_lookup diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml index b02b97f656..aeceeb4e50 100644 --- a/plugins/setoid_ring/newring.ml +++ b/plugins/setoid_ring/newring.ml @@ -327,6 +327,18 @@ module Cmap = Map.Make(Constr) let from_carrier = Summary.ref Cmap.empty ~name:"ring-tac-carrier-table" let from_name = Summary.ref Spmap.empty ~name:"ring-tac-name-table" +let print_rings () = + Feedback.msg_notice (strbrk "The following ring structures have been declared:"); + Spmap.iter (fun fn fi -> + let env = Global.env () in + let sigma = Evd.from_env env in + Feedback.msg_notice + (hov 2 + (Ppconstr.pr_id (Libnames.basename fn)++spc()++ + str"with carrier "++ pr_constr_env env sigma fi.ring_carrier++spc()++ + str"and equivalence relation "++ pr_constr_env env sigma fi.ring_req)) + ) !from_name + let ring_for_carrier r = Cmap.find r !from_carrier let find_ring_structure env sigma l = @@ -824,6 +836,18 @@ let dest_field env evd th_spec = let field_from_carrier = Summary.ref Cmap.empty ~name:"field-tac-carrier-table" let field_from_name = Summary.ref Spmap.empty ~name:"field-tac-name-table" +let print_fields () = + Feedback.msg_notice (strbrk "The following field structures have been declared:"); + Spmap.iter (fun fn fi -> + let env = Global.env () in + let sigma = Evd.from_env env in + Feedback.msg_notice + (hov 2 + (Ppconstr.pr_id (Libnames.basename fn)++spc()++ + str"with carrier "++ pr_constr_env env sigma fi.field_carrier++spc()++ + str"and equivalence relation "++ pr_constr_env env sigma fi.field_req)) + ) !field_from_name + let field_for_carrier r = Cmap.find r !field_from_carrier let find_field_structure env sigma l = diff --git a/plugins/setoid_ring/newring.mli b/plugins/setoid_ring/newring.mli index fcd04a2e73..3a21a82c5c 100644 --- a/plugins/setoid_ring/newring.mli +++ b/plugins/setoid_ring/newring.mli @@ -10,7 +10,6 @@ open Names open EConstr -open Libnames open Constrexpr open Newring_ast @@ -23,7 +22,7 @@ val add_theory : constr_expr -> constr_expr ring_mod list -> unit -val from_name : ring_info Spmap.t ref +val print_rings : unit -> unit val ring_lookup : Geninterp.Val.t -> @@ -35,7 +34,7 @@ val add_field_theory : constr_expr -> constr_expr field_mod list -> unit -val field_from_name : field_info Spmap.t ref +val print_fields : unit -> unit val field_lookup : Geninterp.Val.t -> diff --git a/plugins/ssr/ssrvernac.mlg b/plugins/ssr/ssrvernac.mlg index 08f028465b..8880a6516e 100644 --- a/plugins/ssr/ssrvernac.mlg +++ b/plugins/ssr/ssrvernac.mlg @@ -566,12 +566,10 @@ let print_view_hints env sigma kind l = } VERNAC COMMAND EXTEND PrintView CLASSIFIED AS QUERY -| ![proof] [ "Print" "Hint" "View" ssrviewpos(i) ] -> +| [ "Print" "Hint" "View" ssrviewpos(i) ] -> { - fun ~pstate -> - (* XXX this is incorrect *) - let sigma, env = Option.cata Pfedit.get_current_context - (let e = Global.env () in Evd.from_env e, e) pstate in + let env = Global.env () in + let sigma = Evd.from_env env in (match i with | Some k -> print_view_hints env sigma k (Ssrview.AdaptorDb.get k) @@ -579,8 +577,7 @@ VERNAC COMMAND EXTEND PrintView CLASSIFIED AS QUERY List.iter (fun k -> print_view_hints env sigma k (Ssrview.AdaptorDb.get k)) [ Ssrview.AdaptorDb.Forward; Ssrview.AdaptorDb.Backward; - Ssrview.AdaptorDb.Equivalence ]); - pstate + Ssrview.AdaptorDb.Equivalence ]) } END diff --git a/plugins/syntax/g_numeral.mlg b/plugins/syntax/g_numeral.mlg index 0f0f3953da..5808385723 100644 --- a/plugins/syntax/g_numeral.mlg +++ b/plugins/syntax/g_numeral.mlg @@ -34,23 +34,8 @@ VERNAC ARGUMENT EXTEND numnotoption END VERNAC COMMAND EXTEND NumeralNotation CLASSIFIED AS SIDEFF - | #[ locality = Attributes.locality; ] ![proof][ "Numeral" "Notation" reference(ty) reference(f) reference(g) ":" + | #[ locality = Attributes.locality; ] [ "Numeral" "Notation" reference(ty) reference(f) reference(g) ":" ident(sc) numnotoption(o) ] -> - { (* It is a bug to use the proof context here, but at the request of - * the reviewers we keep this broken behavior for now. The Global env - * should be used instead, and the `env, sigma` parameteter to the - * numeral notation command removed. - *) - fun ~pstate -> - let sigma, env = match pstate with - | None -> - let env = Global.env () in - let sigma = Evd.from_env env in - sigma, env - | Some pstate -> - Pfedit.get_current_context pstate - in - vernac_numeral_notation env sigma (Locality.make_module_locality locality) ty f g (Id.to_string sc) o; - pstate } + { vernac_numeral_notation (Locality.make_module_locality locality) ty f g (Id.to_string sc) o } END diff --git a/plugins/syntax/g_string.mlg b/plugins/syntax/g_string.mlg index cc8c13a84b..1e06cd8ddb 100644 --- a/plugins/syntax/g_string.mlg +++ b/plugins/syntax/g_string.mlg @@ -19,22 +19,7 @@ open Stdarg } VERNAC COMMAND EXTEND StringNotation CLASSIFIED AS SIDEFF - | #[ locality = Attributes.locality; ] ![proof] [ "String" "Notation" reference(ty) reference(f) reference(g) ":" + | #[ locality = Attributes.locality; ] [ "String" "Notation" reference(ty) reference(f) reference(g) ":" ident(sc) ] -> - { (* It is a bug to use the proof context here, but at the request of - * the reviewers we keep this broken behavior for now. The Global env - * should be used instead, and the `env, sigma` parameteter to the - * numeral notation command removed. - *) - fun ~pstate -> - let sigma, env = match pstate with - | None -> - let env = Global.env () in - let sigma = Evd.from_env env in - sigma, env - | Some pstate -> - Pfedit.get_current_context pstate - in - vernac_string_notation env sigma (Locality.make_module_locality locality) ty f g (Id.to_string sc); - pstate } + { vernac_string_notation (Locality.make_module_locality locality) ty f g (Id.to_string sc) } END diff --git a/plugins/syntax/numeral.ml b/plugins/syntax/numeral.ml index ec8c2338fb..b0b6fa69bb 100644 --- a/plugins/syntax/numeral.ml +++ b/plugins/syntax/numeral.ml @@ -101,7 +101,9 @@ let type_error_of g ty = str " to Decimal.int or (option Decimal.int)." ++ fnl () ++ str "Instead of Decimal.int, the types Decimal.uint or Z or Int63.int or Decimal.decimal could be used (you may need to require BinNums or Decimal or Int63 first).") -let vernac_numeral_notation env sigma local ty f g scope opts = +let vernac_numeral_notation local ty f g scope opts = + let env = Global.env () in + let sigma = Evd.from_env env in let dec_ty = locate_decimal () in let z_pos_ty = locate_z () in let int63_ty = locate_int63 () in diff --git a/plugins/syntax/numeral.mli b/plugins/syntax/numeral.mli index b14ed18497..3fc0385f5d 100644 --- a/plugins/syntax/numeral.mli +++ b/plugins/syntax/numeral.mli @@ -14,6 +14,6 @@ open Notation (** * Numeral notation *) -val vernac_numeral_notation : Environ.env -> Evd.evar_map -> locality_flag -> +val vernac_numeral_notation : locality_flag -> qualid -> qualid -> qualid -> Notation_term.scope_name -> numnot_option -> unit diff --git a/plugins/syntax/string_notation.ml b/plugins/syntax/string_notation.ml index 5fae696d58..4234cee1bd 100644 --- a/plugins/syntax/string_notation.ml +++ b/plugins/syntax/string_notation.ml @@ -47,7 +47,9 @@ let type_error_of g ty = (pr_qualid g ++ str " should go from " ++ pr_qualid ty ++ str " to Byte.byte or (option Byte.byte) or (list Byte.byte) or (option (list Byte.byte)).") -let vernac_string_notation env sigma local ty f g scope = +let vernac_string_notation local ty f g scope = + let env = Global.env () in + let sigma = Evd.from_env env in let app x y = mkAppC (x,[y]) in let cref q = mkRefC q in let cbyte = cref (q_byte ()) in diff --git a/plugins/syntax/string_notation.mli b/plugins/syntax/string_notation.mli index e81de603d9..1e25758572 100644 --- a/plugins/syntax/string_notation.mli +++ b/plugins/syntax/string_notation.mli @@ -13,6 +13,6 @@ open Vernacexpr (** * String notation *) -val vernac_string_notation : Environ.env -> Evd.evar_map -> locality_flag -> +val vernac_string_notation : locality_flag -> qualid -> qualid -> qualid -> Notation_term.scope_name -> unit diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml index 51708670f5..4b1b473b33 100644 --- a/tactics/autorewrite.ml +++ b/tactics/autorewrite.ml @@ -75,7 +75,9 @@ let find_matches bas pat = let res = HintDN.search_pattern base pat in List.map snd res -let print_rewrite_hintdb env sigma bas = +let print_rewrite_hintdb bas = + let env = Global.env () in + let sigma = Evd.from_env env in (str "Database " ++ str bas ++ fnl () ++ prlist_with_sep fnl (fun h -> diff --git a/tactics/autorewrite.mli b/tactics/autorewrite.mli index 03e9414e0f..4c6146d745 100644 --- a/tactics/autorewrite.mli +++ b/tactics/autorewrite.mli @@ -42,7 +42,7 @@ val auto_multi_rewrite : ?conds:conditions -> string list -> Locus.clause -> uni val auto_multi_rewrite_with : ?conds:conditions -> unit Proofview.tactic -> string list -> Locus.clause -> unit Proofview.tactic -val print_rewrite_hintdb : Environ.env -> Evd.evar_map -> string -> Pp.t +val print_rewrite_hintdb : string -> Pp.t open Clenv diff --git a/test-suite/output/injection.out b/test-suite/output/injection.out new file mode 100644 index 0000000000..ff40a478f3 --- /dev/null +++ b/test-suite/output/injection.out @@ -0,0 +1,4 @@ +The command has indeed failed with message: +Unexpected pattern. +The command has indeed failed with message: +Unexpected injection pattern. diff --git a/test-suite/output/injection.v b/test-suite/output/injection.v new file mode 100644 index 0000000000..bfd5a67bf5 --- /dev/null +++ b/test-suite/output/injection.v @@ -0,0 +1,8 @@ +(* Test error messages *) + +Goal forall x, (x,0) = (0, S x) -> x = 0. +Fail intros x H; injection H as [= H'] H''. +Fail intros x H; injection H as H' [= H'']. +intros x H; injection H as [= H' H'']. +exact H'. +Qed. diff --git a/theories/Arith/Peano_dec.v b/theories/Arith/Peano_dec.v index ddbc128aa1..6a4a0445b5 100644 --- a/theories/Arith/Peano_dec.v +++ b/theories/Arith/Peano_dec.v @@ -53,7 +53,7 @@ destruct le_mn1; intros le_mn2; destruct le_mn2. now destruct (Nat.nle_succ_diag_l _ le_mn0). + intros def_n0; generalize le_mn1; rewrite def_n0; intros le_mn0. now destruct (Nat.nle_succ_diag_l _ le_mn0). -+ intros def_n0. injection def_n0 as ->. ++ intros def_n0. injection def_n0 as [= ->]. rewrite (UIP_nat _ _ def_n0 eq_refl); simpl. assert (H : le_mn1 = le_mn2). now apply IHn0. diff --git a/theories/FSets/FMapFacts.v b/theories/FSets/FMapFacts.v index e68bc5930d..153842654a 100644 --- a/theories/FSets/FMapFacts.v +++ b/theories/FSets/FMapFacts.v @@ -1988,7 +1988,7 @@ Module OrdProperties (M:S). simpl; intros; try discriminate. intros. destruct a; destruct l; simpl in *. - injection H as -> ->. + injection H as [= -> ->]. inversion_clear H1. red in H; simpl in *; intuition. elim H0; eauto. @@ -2052,7 +2052,7 @@ Module OrdProperties (M:S). generalize (elements_3 m). destruct (elements m). try discriminate. - destruct p; injection H as -> ->; intros H4. + destruct p; injection H as [= -> ->]; intros H4. inversion_clear H1 as [? ? H2|? ? H2]. red in H2; destruct H2; simpl in *; ME.order. inversion_clear H4. rename H1 into H3. diff --git a/theories/FSets/FMapPositive.v b/theories/FSets/FMapPositive.v index b47c99244b..37dd2304da 100644 --- a/theories/FSets/FMapPositive.v +++ b/theories/FSets/FMapPositive.v @@ -277,7 +277,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits. rewrite append_assoc_1; apply in_or_app; right; apply in_cons; apply IHm2; auto. rewrite append_assoc_0; apply in_or_app; left; apply IHm1; auto. - rewrite append_neutral_r; apply in_or_app; injection H as ->; + rewrite append_neutral_r; apply in_or_app; injection H as [= ->]; right; apply in_eq. rewrite append_assoc_1; apply in_or_app; right; apply IHm2; auto. rewrite append_assoc_0; apply in_or_app; left; apply IHm1; auto. @@ -318,7 +318,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits. apply in_or_app. left; apply IHm1; auto. right; destruct (in_inv H0). - injection H1 as -> ->; apply in_eq. + injection H1 as [= -> ->]; apply in_eq. apply in_cons; apply IHm2; auto. left; apply IHm1; auto. right; apply IHm2; auto. @@ -349,7 +349,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits. apply in_or_app. left; apply IHm1; auto. right; destruct (in_inv H0). - injection H1 as -> ->; apply in_eq. + injection H1 as [= -> ->]; apply in_eq. apply in_cons; apply IHm2; auto. left; apply IHm1; auto. right; apply IHm2; auto. @@ -692,7 +692,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits. destruct y2; destruct y0; compute in Hy2; destruct Hy2; subst. red; red; simpl. destruct H0. - injection H0 as H0 _; subst. + injection H0 as [= H0 _]; subst. eapply xelements_bits_lt_1; eauto. apply E.bits_lt_trans with p. eapply xelements_bits_lt_1; eauto. diff --git a/theories/FSets/FSetPositive.v b/theories/FSets/FSetPositive.v index 8a93f38164..d2e10e42a6 100644 --- a/theories/FSets/FSetPositive.v +++ b/theories/FSets/FSetPositive.v @@ -1009,10 +1009,10 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits. destruct o. intros x H. injection H; intros; subst. reflexivity. revert IHl. case choose. - intros p Hp x H. injection H as <-. apply Hp. + intros p Hp x [= <-]. apply Hp. reflexivity. intros _ x. revert IHr. case choose. - intros p Hp H. injection H as <-. apply Hp. + intros p Hp [= <-]. apply Hp. reflexivity. intros. discriminate. Qed. @@ -1068,11 +1068,11 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits. induction s as [| l IHl o r IHr]; simpl. intros. discriminate. intros x. destruct (min_elt l); intros. - injection H as <-. apply IHl. reflexivity. + injection H as [= <-]. apply IHl. reflexivity. destruct o; simpl. - injection H as <-. reflexivity. + injection H as [= <-]. reflexivity. destruct (min_elt r); simpl in *. - injection H as <-. apply IHr. reflexivity. + injection H as [= <-]. apply IHr. reflexivity. discriminate. Qed. @@ -1096,15 +1096,15 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits. induction s as [|l IHl o r IHr]; intros x y H H'. discriminate. simpl in H. case_eq (min_elt l). - intros p Hp. rewrite Hp in H. injection H as <-. + intros p Hp. rewrite Hp in H. injection H as [= <-]. destruct y as [z|z|]; simpl; intro; trivial. apply (IHl p z); trivial. intro Hp; rewrite Hp in H. apply min_elt_3 in Hp. destruct o. - injection H as <-. intros Hl. + injection H as [= <-]. intros Hl. destruct y as [z|z|]; simpl; trivial. elim (Hp _ H'). destruct (min_elt r). - injection H as <-. + injection H as [= <-]. destruct y as [z|z|]. apply (IHr e z); trivial. elim (Hp _ H'). @@ -1121,11 +1121,11 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits. induction s as [| l IHl o r IHr]; simpl. intros. discriminate. intros x. destruct (max_elt r); intros. - injection H as <-. apply IHr. reflexivity. + injection H as [= <-]. apply IHr. reflexivity. destruct o; simpl. - injection H as <-. reflexivity. + injection H as [= <-]. reflexivity. destruct (max_elt l); simpl in *. - injection H as <-. apply IHl. reflexivity. + injection H as [= <-]. apply IHl. reflexivity. discriminate. Qed. @@ -1149,15 +1149,15 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits. induction s as [|l IHl o r IHr]; intros x y H H'. discriminate. simpl in H. case_eq (max_elt r). - intros p Hp. rewrite Hp in H. injection H as <-. + intros p Hp. rewrite Hp in H. injection H as [= <-]. destruct y as [z|z|]; simpl; intro; trivial. apply (IHr p z); trivial. intro Hp; rewrite Hp in H. apply max_elt_3 in Hp. destruct o. - injection H as <-. intros Hl. + injection H as [= <-]. intros Hl. destruct y as [z|z|]; simpl; trivial. elim (Hp _ H'). destruct (max_elt l). - injection H as <-. + injection H as [= <-]. destruct y as [z|z|]. elim (Hp _ H'). apply (IHl e z); trivial. diff --git a/theories/Init/Tactics.v b/theories/Init/Tactics.v index 497cf2550b..7eb717787e 100644 --- a/theories/Init/Tactics.v +++ b/theories/Init/Tactics.v @@ -75,7 +75,7 @@ Ltac case_eq x := generalize (eq_refl x); pattern x at -1; case x. (* use either discriminate or injection on a hypothesis *) -Ltac destr_eq H := discriminate H || (try (injection H as H)). +Ltac destr_eq H := discriminate H || (try (injection H as [= H])). (* Similar variants of destruct *) diff --git a/theories/Lists/List.v b/theories/Lists/List.v index a48e9929c4..f73440eb1a 100644 --- a/theories/Lists/List.v +++ b/theories/Lists/List.v @@ -250,7 +250,7 @@ Section Facts. generalize (app_nil_r l); intros E. rewrite -> E; auto. intros. - injection H as H H0. + injection H as [= H H0]. assert ([] = l ++ a0 :: l0) by auto. apply app_cons_not_nil in H1 as []. Qed. @@ -261,18 +261,14 @@ Section Facts. induction x as [| x l IHl]; [ destruct y as [| a l] | destruct y as [| a l0] ]; simpl; auto. - - intros a b H. - injection H. + - intros a b [= ]. auto. - - intros a0 b H. - injection H as H1 H0. + - intros a0 b [= H1 H0]. apply app_cons_not_nil in H0 as []. - - intros a b H. - injection H as H1 H0. + - intros a b [= H1 H0]. assert ([] = l ++ [a]) by auto. apply app_cons_not_nil in H as []. - - intros a0 b H. - injection H as <- H0. + - intros a0 b [= <- H0]. destruct (IHl l0 a0 b H0) as (<-,<-). split; auto. Qed. @@ -336,7 +332,7 @@ Section Facts. absurd (length (x1 :: l1 ++ l) <= length l). simpl; rewrite app_length; auto with arith. rewrite H; auto with arith. - injection H as H H0; f_equal; eauto. + injection H as [= H H0]; f_equal; eauto. Qed. End Facts. @@ -519,7 +515,7 @@ Section Elts. Proof. revert l. induction n as [|n IH]; intros [|x l] H; simpl in *; try easy. - - exists nil; exists l. now injection H as ->. + - exists nil; exists l. now injection H as [= ->]. - destruct (IH _ H) as (l1 & l2 & H1 & H2). exists (x::l1); exists l2; simpl; split; now f_equal. Qed. @@ -1243,7 +1239,7 @@ End Fold_Right_Recursor. Proof. induction l as [|a l IH]; simpl; [easy| ]. case_eq (f a); intros Ha Eq. - * injection Eq as ->; auto. + * injection Eq as [= ->]; auto. * destruct (IH Eq); auto. Qed. @@ -1304,10 +1300,10 @@ End Fold_Right_Recursor. forall x:A, In x l <-> In x l1 \/ In x l2. Proof. revert l1 l2. induction l as [| a l' Hrec]; simpl; intros l1 l2 Eq x. - - injection Eq as <- <-. tauto. + - injection Eq as [= <- <-]. tauto. - destruct (partition l') as (left, right). specialize (Hrec left right eq_refl x). - destruct (f a); injection Eq as <- <-; simpl; tauto. + destruct (f a); injection Eq as [= <- <-]; simpl; tauto. Qed. End Bool. @@ -1483,7 +1479,7 @@ End Fold_Right_Recursor. destruct (in_app_or _ _ _ H); clear H. destruct (in_map_iff (fun y : B => (a, y)) l' (x,y)) as (H1,_). destruct (H1 H0) as (z,(H2,H3)); clear H0 H1. - injection H2 as -> ->; intuition. + injection H2 as [= -> ->]; intuition. intuition. Qed. diff --git a/theories/Logic/WeakFan.v b/theories/Logic/WeakFan.v index c9822f47dc..13f63c5cbc 100644 --- a/theories/Logic/WeakFan.v +++ b/theories/Logic/WeakFan.v @@ -64,7 +64,7 @@ induction l1, l2. - discriminate. - discriminate. - intros H (HY1,H1) (HY2,H2). - injection H as H. + injection H as [= H]. pose proof (IHl1 l2 H HY1 HY2). clear HY1 HY2 H IHl1. subst l1. f_equal. diff --git a/theories/MSets/MSetPositive.v b/theories/MSets/MSetPositive.v index a726eebd31..330c7959ac 100644 --- a/theories/MSets/MSetPositive.v +++ b/theories/MSets/MSetPositive.v @@ -910,10 +910,10 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits. destruct o. intros x H. injection H; intros; subst. reflexivity. revert IHl. case choose. - intros p Hp x H. injection H as <-. apply Hp. + intros p Hp x [= <-]. apply Hp. reflexivity. intros _ x. revert IHr. case choose. - intros p Hp H. injection H as <-. apply Hp. + intros p Hp [= <-]. apply Hp. reflexivity. intros. discriminate. Qed. @@ -970,11 +970,11 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits. induction s as [| l IHl o r IHr]; simpl. intros. discriminate. intros x. destruct (min_elt l); intros. - injection H as <-. apply IHl. reflexivity. + injection H as [= <-]. apply IHl. reflexivity. destruct o; simpl. - injection H as <-. reflexivity. + injection H as [= <-]. reflexivity. destruct (min_elt r); simpl in *. - injection H as <-. apply IHr. reflexivity. + injection H as [= <-]. apply IHr. reflexivity. discriminate. Qed. @@ -998,15 +998,15 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits. induction s as [|l IHl o r IHr]; intros x y H H'. discriminate. simpl in H. case_eq (min_elt l). - intros p Hp. rewrite Hp in H. injection H as <-. + intros p Hp. rewrite Hp in H. injection H as [= <-]. destruct y as [z|z|]; simpl; intro; trivial. apply (IHl p z); trivial. intro Hp; rewrite Hp in H. apply min_elt_spec3 in Hp. destruct o. - injection H as <-. intros Hl. + injection H as [= <-]. intros Hl. destruct y as [z|z|]; simpl; trivial. elim (Hp _ H'). destruct (min_elt r). - injection H as <-. + injection H as [= <-]. destruct y as [z|z|]. apply (IHr e z); trivial. elim (Hp _ H'). @@ -1023,11 +1023,11 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits. induction s as [| l IHl o r IHr]; simpl. intros. discriminate. intros x. destruct (max_elt r); intros. - injection H as <-. apply IHr. reflexivity. + injection H as [= <-]. apply IHr. reflexivity. destruct o; simpl. - injection H as <-. reflexivity. + injection H as [= <-]. reflexivity. destruct (max_elt l); simpl in *. - injection H as <-. apply IHl. reflexivity. + injection H as [= <-]. apply IHl. reflexivity. discriminate. Qed. @@ -1051,15 +1051,15 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits. induction s as [|l IHl o r IHr]; intros x y H H'. discriminate. simpl in H. case_eq (max_elt r). - intros p Hp. rewrite Hp in H. injection H as <-. + intros p Hp. rewrite Hp in H. injection H as [= <-]. destruct y as [z|z|]; simpl; intro; trivial. apply (IHr p z); trivial. intro Hp; rewrite Hp in H. apply max_elt_spec3 in Hp. destruct o. - injection H as <-. intros Hl. + injection H as [= <-]. intros Hl. destruct y as [z|z|]; simpl; trivial. elim (Hp _ H'). destruct (max_elt l). - injection H as <-. + injection H as [= <-]. destruct y as [z|z|]. elim (Hp _ H'). apply (IHl e z); trivial. diff --git a/theories/MSets/MSetRBT.v b/theories/MSets/MSetRBT.v index f9105fdf74..a2ffd2050e 100644 --- a/theories/MSets/MSetRBT.v +++ b/theories/MSets/MSetRBT.v @@ -1950,7 +1950,7 @@ Module Make (X: Orders.OrderedType) <: generalize (fun x s' => @Raw.remove_min_spec1 s x s' Hs). set (P := Raw.remove_min_ok s). clearbody P. destruct (Raw.remove_min s) as [(x0,s0)|]; try easy. - intros H U. injection U as -> <-. simpl. + intros H [= -> <-]. simpl. destruct (H x s0); auto. subst; intuition. Qed. diff --git a/theories/Numbers/Cyclic/ZModulo/ZModulo.v b/theories/Numbers/Cyclic/ZModulo/ZModulo.v index 4bcd22543f..94da55b3f3 100644 --- a/theories/Numbers/Cyclic/ZModulo/ZModulo.v +++ b/theories/Numbers/Cyclic/ZModulo/ZModulo.v @@ -372,7 +372,7 @@ Section ZModulo. assert (Z.div_eucl ([|x|]*[|y|]) wB = (([|x|]*[|y|])/wB,([|x|]*[|y|]) mod wB)). unfold Z.modulo, Z.div; destruct Z.div_eucl; auto. generalize (Z_div_mod ([|x|]*[|y|]) wB wB_pos); destruct Z.div_eucl as (h,l). - destruct 1; injection H as ? ?. + destruct 1; injection H as [= ? ?]. rewrite H0. assert ([|l|] = l). apply Zmod_small; auto. @@ -414,7 +414,7 @@ Section ZModulo. unfold Z.modulo, Z.div; destruct Z.div_eucl; auto. generalize (Z_div_mod [|a|] [|b|] H0). destruct Z.div_eucl as (q,r); destruct 1; intros. - injection H1 as ? ?. + injection H1 as [= ? ?]. assert ([|r|]=r). apply Zmod_small; generalize (Z_mod_lt b wB wB_pos); fold [|b|]; auto with zarith. @@ -525,7 +525,7 @@ Section ZModulo. unfold Z.modulo, Z.div; destruct Z.div_eucl; auto. generalize (Z_div_mod a [|b|] H3). destruct Z.div_eucl as (q,r); destruct 1; intros. - injection H4 as ? ?. + injection H4 as [= ? ?]. assert ([|r|]=r). apply Zmod_small; generalize (Z_mod_lt b wB wB_pos); fold [|b|]; auto with zarith. diff --git a/theories/QArith/Qcanon.v b/theories/QArith/Qcanon.v index f18fca99a0..9eae960086 100644 --- a/theories/QArith/Qcanon.v +++ b/theories/QArith/Qcanon.v @@ -43,10 +43,10 @@ Proof. generalize (Z.gcd_nonneg a (Zpos b)) (Z.ggcd_correct_divisors a (Zpos b)). rewrite <- Z.ggcd_gcd. destruct Z.ggcd as (g,(aa,bb)); simpl in *. - injection H as <- <-. intros H (_,H'). + injection H as [= <- <-]. intros H (_,H'). destruct g as [|g|g]; [ discriminate | | now elim H ]. destruct bb as [|b|b]; simpl in *; try discriminate. - injection H' as H'. f_equal. + injection H' as [= H']. f_equal. apply Pos.mul_reg_r with b. now rewrite Pos.mul_1_l. Qed. @@ -87,7 +87,7 @@ Arguments Q2Qc q%Q. Lemma Q2Qc_eq_iff (q q' : Q) : Q2Qc q = Q2Qc q' <-> q == q'. Proof. split; intro H. - - now injection H as H%Qred_eq_iff. + - now injection H as [= H%Qred_eq_iff]. - apply Qc_is_canon. simpl. now rewrite H. Qed. @@ -269,7 +269,7 @@ Theorem Qcmult_integral : forall x y, x*y=0 -> x=0 \/ y=0. Proof. intros. destruct (Qmult_integral x y); try qc; auto. - injection H as H. + injection H as [= H]. rewrite <- (Qred_correct (x*y)). rewrite <- (Qred_correct 0). rewrite H; auto with qarith. diff --git a/theories/Sorting/Permutation.v b/theories/Sorting/Permutation.v index f5bc9eee4e..170c221a45 100644 --- a/theories/Sorting/Permutation.v +++ b/theories/Sorting/Permutation.v @@ -304,7 +304,7 @@ Qed. Lemma Permutation_length_1_inv: forall a l, Permutation [a] l -> l = [a]. Proof. intros a l H; remember [a] as m in H. - induction H; try (injection Heqm as -> ->); + induction H; try (injection Heqm as [= -> ->]); discriminate || auto. apply Permutation_nil in H as ->; trivial. Qed. @@ -312,7 +312,7 @@ Qed. Lemma Permutation_length_1: forall a b, Permutation [a] [b] -> a = b. Proof. intros a b H. - apply Permutation_length_1_inv in H; injection H as ->; trivial. + apply Permutation_length_1_inv in H; injection H as [= ->]; trivial. Qed. Lemma Permutation_length_2_inv : @@ -320,7 +320,7 @@ Lemma Permutation_length_2_inv : Proof. intros a1 a2 l H; remember [a1;a2] as m in H. revert a1 a2 Heqm. - induction H; intros; try (injection Heqm as ? ?; subst); + induction H; intros; try (injection Heqm as [= ? ?]; subst); discriminate || (try tauto). apply Permutation_length_1_inv in H as ->; left; auto. apply IHPermutation1 in Heqm as [H1|H1]; apply IHPermutation2 in H1 as []; @@ -332,7 +332,7 @@ Lemma Permutation_length_2 : a1 = b1 /\ a2 = b2 \/ a1 = b2 /\ a2 = b1. Proof. intros a1 b1 a2 b2 H. - apply Permutation_length_2_inv in H as [H|H]; injection H as -> ->; auto. + apply Permutation_length_2_inv in H as [H|H]; injection H as [= -> ->]; auto. Qed. Lemma NoDup_Permutation l l' : NoDup l -> NoDup l' -> diff --git a/theories/Strings/String.v b/theories/Strings/String.v index 08ccfac877..85bde6a4df 100644 --- a/theories/Strings/String.v +++ b/theories/Strings/String.v @@ -123,7 +123,7 @@ intros H; generalize (H O); simpl; intros H1; inversion H1. case (Rec s). intros H0; rewrite H0; auto. intros n; exact (H (S n)). -intros H; injection H as H1 H2. +intros [= H1 H2]. rewrite H2; trivial. rewrite H1; auto. Qed. @@ -290,14 +290,14 @@ intros n m s1 s2; generalize n m s1; clear n m s1; elim s2; simpl; auto. intros n; case n; simpl; auto. intros m s1; case s1; simpl; auto. -intros H; injection H as <-; auto. +intros [= <-]; auto. intros; discriminate. intros; discriminate. intros b s2' Rec n m s1. case n; simpl; auto. generalize (prefix_correct s1 (String b s2')); case (prefix s1 (String b s2')). -intros H0 H; injection H as <-; auto. +intros H0 [= <-]; auto. case H0; simpl; auto. case m; simpl; auto. case (index O s1 s2'); intros; discriminate. @@ -323,7 +323,7 @@ intros n m s1 s2; generalize n m s1; clear n m s1; elim s2; simpl; auto. intros n; case n; simpl; auto. intros m s1; case s1; simpl; auto. -intros H; injection H as <-. +intros [= <-]. intros p H0 H2; inversion H2. intros; discriminate. intros; discriminate. @@ -331,7 +331,7 @@ intros b s2' Rec n m s1. case n; simpl; auto. generalize (prefix_correct s1 (String b s2')); case (prefix s1 (String b s2')). -intros H0 H; injection H as <-; auto. +intros H0 [= <-]; auto. intros p H2 H3; inversion H3. case m; simpl; auto. case (index 0 s1 s2'); intros; discriminate. diff --git a/theories/Wellfounded/Lexicographic_Product.v b/theories/Wellfounded/Lexicographic_Product.v index b2d08186ea..60db536dce 100644 --- a/theories/Wellfounded/Lexicographic_Product.v +++ b/theories/Wellfounded/Lexicographic_Product.v @@ -46,11 +46,11 @@ Section WfLexicographic_Product. apply H2. auto with sets. - + injection H1 as <- _. - injection H3 as <- _; auto with sets. + + injection H1 as [= <- _]. + injection H3 as [= <- _]; auto with sets. - rewrite <- H1. - injection H3 as -> H3. + injection H3 as [= -> H3]. apply IHAcc0. elim inj_pair2 with A B x y' x0; assumption. Defined. diff --git a/toplevel/coqcargs.ml b/toplevel/coqcargs.ml index 2279ce5505..63c37e2251 100644 --- a/toplevel/coqcargs.ml +++ b/toplevel/coqcargs.ml @@ -63,7 +63,10 @@ let check_compilation_output_name_consistency args = prerr_endline ("file have to be compiled") | _ -> () +let is_dash_argument s = String.length s > 0 && s.[0] = '-' + let add_compile ?echo copts s = + if is_dash_argument s then (prerr_endline ("Unknown option " ^ s); exit 1); (* make the file name explicit; needed not to break up Coq loadpath stuff. *) let echo = Option.default copts.echo echo in let s = |