diff options
author | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-03-04 11:16:03 +0100 |
---|---|---|
committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-03-04 14:52:53 +0100 |
commit | d5656a6c28f79d59590d4fde60c5158a649d1b65 (patch) | |
tree | eac22126e5577742b22d731e53e9b49e81d40095 /theories | |
parent | 143bb68613bcb314e2feffd643f539fba9cd3912 (diff) |
Making parentheses mandatory in tactic scopes.
Diffstat (limited to 'theories')
-rw-r--r-- | theories/Classes/CMorphisms.v | 2 | ||||
-rw-r--r-- | theories/Classes/Morphisms.v | 2 | ||||
-rw-r--r-- | theories/Classes/SetoidTactics.v | 16 | ||||
-rw-r--r-- | theories/Numbers/Cyclic/Int31/Ring31.v | 20 | ||||
-rw-r--r-- | theories/Numbers/Integer/BigZ/BigZ.v | 22 | ||||
-rw-r--r-- | theories/Numbers/Natural/BigN/BigN.v | 24 | ||||
-rw-r--r-- | theories/Numbers/Rational/BigQ/BigQ.v | 14 | ||||
-rw-r--r-- | theories/Program/Equality.v | 4 | ||||
-rw-r--r-- | theories/Program/Tactics.v | 2 | ||||
-rw-r--r-- | theories/Reals/Ranalysis_reg.v | 100 | ||||
-rw-r--r-- | theories/ZArith/Int.v | 14 | ||||
-rw-r--r-- | theories/ZArith/Zsqrt_compat.v | 4 |
12 files changed, 112 insertions, 112 deletions
diff --git a/theories/Classes/CMorphisms.v b/theories/Classes/CMorphisms.v index c41eb2fa2..627a1a495 100644 --- a/theories/Classes/CMorphisms.v +++ b/theories/Classes/CMorphisms.v @@ -452,7 +452,7 @@ Ltac partial_application_tactic := let rec do_partial_apps H m cont := match m with | ?m' ?x => class_apply @Reflexive_partial_app_morphism ; - [(do_partial_apps H m' ltac:idtac)|clear H] + [(do_partial_apps H m' ltac:(idtac))|clear H] | _ => cont end in diff --git a/theories/Classes/Morphisms.v b/theories/Classes/Morphisms.v index 8d942d908..81b31d783 100644 --- a/theories/Classes/Morphisms.v +++ b/theories/Classes/Morphisms.v @@ -465,7 +465,7 @@ Ltac partial_application_tactic := let rec do_partial_apps H m cont := match m with | ?m' ?x => class_apply @Reflexive_partial_app_morphism ; - [(do_partial_apps H m' ltac:idtac)|clear H] + [(do_partial_apps H m' ltac:(idtac))|clear H] | _ => cont end in diff --git a/theories/Classes/SetoidTactics.v b/theories/Classes/SetoidTactics.v index 145d451f0..190397ae4 100644 --- a/theories/Classes/SetoidTactics.v +++ b/theories/Classes/SetoidTactics.v @@ -77,23 +77,23 @@ Tactic Notation "setoid_replace" constr(x) "with" constr(y) Tactic Notation "setoid_replace" constr(x) "with" constr(y) "by" tactic3(t) := - setoidreplace (default_relation x y) ltac:t. + setoidreplace (default_relation x y) ltac:(t). Tactic Notation "setoid_replace" constr(x) "with" constr(y) "at" int_or_var_list(o) "by" tactic3(t) := - setoidreplaceat (default_relation x y) ltac:t o. + setoidreplaceat (default_relation x y) ltac:(t) o. Tactic Notation "setoid_replace" constr(x) "with" constr(y) "in" hyp(id) "by" tactic3(t) := - setoidreplacein (default_relation x y) id ltac:t. + setoidreplacein (default_relation x y) id ltac:(t). Tactic Notation "setoid_replace" constr(x) "with" constr(y) "in" hyp(id) "at" int_or_var_list(o) "by" tactic3(t) := - setoidreplaceinat (default_relation x y) id ltac:t o. + setoidreplaceinat (default_relation x y) id ltac:(t) o. Tactic Notation "setoid_replace" constr(x) "with" constr(y) "using" "relation" constr(rel) := @@ -107,13 +107,13 @@ Tactic Notation "setoid_replace" constr(x) "with" constr(y) Tactic Notation "setoid_replace" constr(x) "with" constr(y) "using" "relation" constr(rel) "by" tactic3(t) := - setoidreplace (rel x y) ltac:t. + setoidreplace (rel x y) ltac:(t). Tactic Notation "setoid_replace" constr(x) "with" constr(y) "using" "relation" constr(rel) "at" int_or_var_list(o) "by" tactic3(t) := - setoidreplaceat (rel x y) ltac:t o. + setoidreplaceat (rel x y) ltac:(t) o. Tactic Notation "setoid_replace" constr(x) "with" constr(y) "using" "relation" constr(rel) @@ -130,14 +130,14 @@ Tactic Notation "setoid_replace" constr(x) "with" constr(y) "using" "relation" constr(rel) "in" hyp(id) "by" tactic3(t) := - setoidreplacein (rel x y) id ltac:t. + setoidreplacein (rel x y) id ltac:(t). Tactic Notation "setoid_replace" constr(x) "with" constr(y) "using" "relation" constr(rel) "in" hyp(id) "at" int_or_var_list(o) "by" tactic3(t) := - setoidreplaceinat (rel x y) id ltac:t o. + setoidreplaceinat (rel x y) id ltac:(t) o. (** The [add_morphism_tactic] tactic is run at each [Add Morphism] command before giving the hand back to the user to discharge the diff --git a/theories/Numbers/Cyclic/Int31/Ring31.v b/theories/Numbers/Cyclic/Int31/Ring31.v index 215b8bd58..d160f5f1d 100644 --- a/theories/Numbers/Cyclic/Int31/Ring31.v +++ b/theories/Numbers/Cyclic/Int31/Ring31.v @@ -19,13 +19,13 @@ Local Open Scope list_scope. Ltac isInt31cst_lst l := match l with - | nil => constr:true + | nil => constr:(true) | ?t::?l => match t with | D1 => isInt31cst_lst l | D0 => isInt31cst_lst l - | _ => constr:false + | _ => constr:(false) end - | _ => constr:false + | _ => constr:(false) end. Ltac isInt31cst t := @@ -38,17 +38,17 @@ Ltac isInt31cst t := ::i11::i12::i13::i14::i15::i16::i17::i18::i19::i20 ::i21::i22::i23::i24::i25::i26::i27::i28::i29::i30::nil) in isInt31cst_lst l - | Int31.On => constr:true - | Int31.In => constr:true - | Int31.Tn => constr:true - | Int31.Twon => constr:true - | _ => constr:false + | Int31.On => constr:(true) + | Int31.In => constr:(true) + | Int31.Tn => constr:(true) + | Int31.Twon => constr:(true) + | _ => constr:(false) end. Ltac Int31cst t := match isInt31cst t with - | true => constr:t - | false => constr:NotConstant + | true => constr:(t) + | false => constr:(NotConstant) end. (** The generic ring structure inferred from the Cyclic structure *) diff --git a/theories/Numbers/Integer/BigZ/BigZ.v b/theories/Numbers/Integer/BigZ/BigZ.v index ec495d094..56cb9bbc2 100644 --- a/theories/Numbers/Integer/BigZ/BigZ.v +++ b/theories/Numbers/Integer/BigZ/BigZ.v @@ -148,26 +148,26 @@ Ltac isBigZcst t := match t with | BigZ.Pos ?t => isBigNcst t | BigZ.Neg ?t => isBigNcst t - | BigZ.zero => constr:true - | BigZ.one => constr:true - | BigZ.two => constr:true - | BigZ.minus_one => constr:true - | _ => constr:false + | BigZ.zero => constr:(true) + | BigZ.one => constr:(true) + | BigZ.two => constr:(true) + | BigZ.minus_one => constr:(true) + | _ => constr:(false) end. Ltac BigZcst t := match isBigZcst t with - | true => constr:t - | false => constr:NotConstant + | true => constr:(t) + | false => constr:(NotConstant) end. Ltac BigZ_to_N t := match t with | BigZ.Pos ?t => BigN_to_N t - | BigZ.zero => constr:0%N - | BigZ.one => constr:1%N - | BigZ.two => constr:2%N - | _ => constr:NotConstant + | BigZ.zero => constr:(0%N) + | BigZ.one => constr:(1%N) + | BigZ.two => constr:(2%N) + | _ => constr:(NotConstant) end. (** Registration for the "ring" tactic *) diff --git a/theories/Numbers/Natural/BigN/BigN.v b/theories/Numbers/Natural/BigN/BigN.v index 29a1145e0..ec1017f50 100644 --- a/theories/Numbers/Natural/BigN/BigN.v +++ b/theories/Numbers/Natural/BigN/BigN.v @@ -119,10 +119,10 @@ Qed. Ltac isStaticWordCst t := match t with - | W0 => constr:true + | W0 => constr:(true) | WW ?t1 ?t2 => match isStaticWordCst t1 with - | false => constr:false + | false => constr:(false) | true => isStaticWordCst t2 end | _ => isInt31cst t @@ -139,30 +139,30 @@ Ltac isBigNcst t := | BigN.N6 ?t => isStaticWordCst t | BigN.Nn ?n ?t => match isnatcst n with | true => isStaticWordCst t - | false => constr:false + | false => constr:(false) end - | BigN.zero => constr:true - | BigN.one => constr:true - | BigN.two => constr:true - | _ => constr:false + | BigN.zero => constr:(true) + | BigN.one => constr:(true) + | BigN.two => constr:(true) + | _ => constr:(false) end. Ltac BigNcst t := match isBigNcst t with - | true => constr:t - | false => constr:NotConstant + | true => constr:(t) + | false => constr:(NotConstant) end. Ltac BigN_to_N t := match isBigNcst t with | true => eval vm_compute in (BigN.to_N t) - | false => constr:NotConstant + | false => constr:(NotConstant) end. Ltac Ncst t := match isNcst t with - | true => constr:t - | false => constr:NotConstant + | true => constr:(t) + | false => constr:(NotConstant) end. (** Registration for the "ring" tactic *) diff --git a/theories/Numbers/Rational/BigQ/BigQ.v b/theories/Numbers/Rational/BigQ/BigQ.v index fe38ea4f2..850afe534 100644 --- a/theories/Numbers/Rational/BigQ/BigQ.v +++ b/theories/Numbers/Rational/BigQ/BigQ.v @@ -104,18 +104,18 @@ Ltac isBigQcst t := | BigQ.Qz ?t => isBigZcst t | BigQ.Qq ?n ?d => match isBigZcst n with | true => isBigNcst d - | false => constr:false + | false => constr:(false) end - | BigQ.zero => constr:true - | BigQ.one => constr:true - | BigQ.minus_one => constr:true - | _ => constr:false + | BigQ.zero => constr:(true) + | BigQ.one => constr:(true) + | BigQ.minus_one => constr:(true) + | _ => constr:(false) end. Ltac BigQcst t := match isBigQcst t with - | true => constr:t - | false => constr:NotConstant + | true => constr:(t) + | false => constr:(NotConstant) end. Add Field BigQfield : BigQfieldth diff --git a/theories/Program/Equality.v b/theories/Program/Equality.v index 27e1ca844..17f05c511 100644 --- a/theories/Program/Equality.v +++ b/theories/Program/Equality.v @@ -238,8 +238,8 @@ Ltac inject_left H := Ltac inject_right H := progress (inversion H ; subst_right_no_fail ; clear_dups) ; clear H. -Ltac autoinjections_left := repeat autoinjection ltac:inject_left. -Ltac autoinjections_right := repeat autoinjection ltac:inject_right. +Ltac autoinjections_left := repeat autoinjection ltac:(inject_left). +Ltac autoinjections_right := repeat autoinjection ltac:(inject_right). Ltac simpl_depind := subst_no_fail ; autoinjections ; try discriminates ; simpl_JMeq ; simpl_existTs ; simplify_IH_hyps. diff --git a/theories/Program/Tactics.v b/theories/Program/Tactics.v index 66ca3e577..7384790da 100644 --- a/theories/Program/Tactics.v +++ b/theories/Program/Tactics.v @@ -252,7 +252,7 @@ Ltac autoinjection tac := Ltac inject H := progress (inversion H ; subst*; clear_dups) ; clear H. -Ltac autoinjections := repeat (clear_dups ; autoinjection ltac:inject). +Ltac autoinjections := repeat (clear_dups ; autoinjection ltac:(inject)). (** Destruct an hypothesis by first copying it to avoid dependencies. *) diff --git a/theories/Reals/Ranalysis_reg.v b/theories/Reals/Ranalysis_reg.v index 2465f0399..e57af7311 100644 --- a/theories/Reals/Ranalysis_reg.v +++ b/theories/Reals/Ranalysis_reg.v @@ -35,7 +35,7 @@ Qed. (**********) Ltac intro_hyp_glob trm := - match constr:trm with + match constr:(trm) with | (?X1 + ?X2)%F => match goal with | |- (derivable _) => intro_hyp_glob X1; intro_hyp_glob X2 @@ -55,7 +55,7 @@ Ltac intro_hyp_glob trm := | _ => idtac end | (?X1 / ?X2)%F => - let aux := constr:X2 in + let aux := constr:(X2) in match goal with | _:(forall x0:R, aux x0 <> 0) |- (derivable _) => intro_hyp_glob X1; intro_hyp_glob X2 @@ -82,7 +82,7 @@ Ltac intro_hyp_glob trm := | _ => idtac end | (/ ?X1)%F => - let aux := constr:X1 in + let aux := constr:(X1) in match goal with | _:(forall x0:R, aux x0 <> 0) |- (derivable _) => intro_hyp_glob X1 @@ -108,7 +108,7 @@ Ltac intro_hyp_glob trm := | (pow_fct _) => idtac | Rabs => idtac | ?X1 => - let p := constr:X1 in + let p := constr:(X1) in match goal with | _:(derivable p) |- _ => idtac | |- (derivable p) => idtac @@ -130,7 +130,7 @@ Ltac intro_hyp_glob trm := (**********) Ltac intro_hyp_pt trm pt := - match constr:trm with + match constr:(trm) with | (?X1 + ?X2)%F => match goal with | |- (derivable_pt _ _) => intro_hyp_pt X1 pt; intro_hyp_pt X2 pt @@ -156,7 +156,7 @@ Ltac intro_hyp_pt trm pt := | _ => idtac end | (?X1 / ?X2)%F => - let aux := constr:X2 in + let aux := constr:(X2) in match goal with | _:(aux pt <> 0) |- (derivable_pt _ _) => intro_hyp_pt X1 pt; intro_hyp_pt X2 pt @@ -202,7 +202,7 @@ Ltac intro_hyp_pt trm pt := | _ => idtac end | (/ ?X1)%F => - let aux := constr:X1 in + let aux := constr:(X1) in match goal with | _:(aux pt <> 0) |- (derivable_pt _ _) => intro_hyp_pt X1 pt @@ -249,7 +249,7 @@ Ltac intro_hyp_pt trm pt := | _ => idtac end | ?X1 => - let p := constr:X1 in + let p := constr:(X1) in match goal with | _:(derivable_pt p pt) |- _ => idtac | |- (derivable_pt p pt) => idtac @@ -578,89 +578,89 @@ Ltac is_cont_glob := (**********) Ltac rew_term trm := - match constr:trm with + match constr:(trm) with | (?X1 + ?X2) => let p1 := rew_term X1 with p2 := rew_term X2 in - match constr:p1 with + match constr:(p1) with | (fct_cte ?X3) => - match constr:p2 with + match constr:(p2) with | (fct_cte ?X4) => constr:(fct_cte (X3 + X4)) - | _ => constr:(p1 + p2)%F + | _ => constr:((p1 + p2)%F) end - | _ => constr:(p1 + p2)%F + | _ => constr:((p1 + p2)%F) end | (?X1 - ?X2) => let p1 := rew_term X1 with p2 := rew_term X2 in - match constr:p1 with + match constr:(p1) with | (fct_cte ?X3) => - match constr:p2 with + match constr:(p2) with | (fct_cte ?X4) => constr:(fct_cte (X3 - X4)) - | _ => constr:(p1 - p2)%F + | _ => constr:((p1 - p2)%F) end - | _ => constr:(p1 - p2)%F + | _ => constr:((p1 - p2)%F) end | (?X1 / ?X2) => let p1 := rew_term X1 with p2 := rew_term X2 in - match constr:p1 with + match constr:(p1) with | (fct_cte ?X3) => - match constr:p2 with + match constr:(p2) with | (fct_cte ?X4) => constr:(fct_cte (X3 / X4)) - | _ => constr:(p1 / p2)%F + | _ => constr:((p1 / p2)%F) end | _ => - match constr:p2 with - | (fct_cte ?X4) => constr:(p1 * fct_cte (/ X4))%F - | _ => constr:(p1 / p2)%F + match constr:(p2) with + | (fct_cte ?X4) => constr:((p1 * fct_cte (/ X4))%F) + | _ => constr:((p1 / p2)%F) end end | (?X1 * / ?X2) => let p1 := rew_term X1 with p2 := rew_term X2 in - match constr:p1 with + match constr:(p1) with | (fct_cte ?X3) => - match constr:p2 with + match constr:(p2) with | (fct_cte ?X4) => constr:(fct_cte (X3 / X4)) - | _ => constr:(p1 / p2)%F + | _ => constr:((p1 / p2)%F) end | _ => - match constr:p2 with - | (fct_cte ?X4) => constr:(p1 * fct_cte (/ X4))%F - | _ => constr:(p1 / p2)%F + match constr:(p2) with + | (fct_cte ?X4) => constr:((p1 * fct_cte (/ X4))%F) + | _ => constr:((p1 / p2)%F) end end | (?X1 * ?X2) => let p1 := rew_term X1 with p2 := rew_term X2 in - match constr:p1 with + match constr:(p1) with | (fct_cte ?X3) => - match constr:p2 with + match constr:(p2) with | (fct_cte ?X4) => constr:(fct_cte (X3 * X4)) - | _ => constr:(p1 * p2)%F + | _ => constr:((p1 * p2)%F) end - | _ => constr:(p1 * p2)%F + | _ => constr:((p1 * p2)%F) end | (- ?X1) => let p := rew_term X1 in - match constr:p with + match constr:(p) with | (fct_cte ?X2) => constr:(fct_cte (- X2)) - | _ => constr:(- p)%F + | _ => constr:((- p)%F) end | (/ ?X1) => let p := rew_term X1 in - match constr:p with + match constr:(p) with | (fct_cte ?X2) => constr:(fct_cte (/ X2)) - | _ => constr:(/ p)%F + | _ => constr:((/ p)%F) end - | (?X1 AppVar) => constr:X1 + | (?X1 AppVar) => constr:(X1) | (?X1 ?X2) => let p := rew_term X2 in - match constr:p with + match constr:(p) with | (fct_cte ?X3) => constr:(fct_cte (X1 X3)) | _ => constr:(comp X1 p) end - | AppVar => constr:id + | AppVar => constr:(id) | (AppVar ^ ?X1) => constr:(pow_fct X1) | (?X1 ^ ?X2) => let p := rew_term X1 in - match constr:p with + match constr:(p) with | (fct_cte ?X3) => constr:(fct_cte (pow_fct X2 X3)) | _ => constr:(comp (pow_fct X2) p) end @@ -669,7 +669,7 @@ Ltac rew_term trm := (**********) Ltac deriv_proof trm pt := - match constr:trm with + match constr:(trm) with | (?X1 + ?X2)%F => let p1 := deriv_proof X1 pt with p2 := deriv_proof X2 pt in constr:(derivable_pt_plus X1 X2 pt p1 p2) @@ -684,14 +684,14 @@ Ltac deriv_proof trm pt := | id:(?X2 pt <> 0) |- _ => let p1 := deriv_proof X1 pt with p2 := deriv_proof X2 pt in constr:(derivable_pt_div X1 X2 pt p1 p2 id) - | _ => constr:False + | _ => constr:(False) end | (/ ?X1)%F => match goal with | id:(?X1 pt <> 0) |- _ => let p1 := deriv_proof X1 pt in constr:(derivable_pt_inv X1 pt p1 id) - | _ => constr:False + | _ => constr:(False) end | (comp ?X1 ?X2) => let pt_f1 := eval cbv beta in (X2 pt) in @@ -710,21 +710,21 @@ Ltac deriv_proof trm pt := | sqrt => match goal with | id:(0 < pt) |- _ => constr:(derivable_pt_sqrt pt id) - | _ => constr:False + | _ => constr:(False) end | (fct_cte ?X1) => constr:(derivable_pt_const X1 pt) | ?X1 => - let aux := constr:X1 in + let aux := constr:(X1) in match goal with - | id:(derivable_pt aux pt) |- _ => constr:id + | id:(derivable_pt aux pt) |- _ => constr:(id) | id:(derivable aux) |- _ => constr:(id pt) - | _ => constr:False + | _ => constr:(False) end end. (**********) Ltac simplify_derive trm pt := - match constr:trm with + match constr:(trm) with | (?X1 + ?X2)%F => try rewrite derive_pt_plus; simplify_derive X1 pt; simplify_derive X2 pt @@ -753,7 +753,7 @@ Ltac simplify_derive trm pt := | Rsqr => try rewrite derive_pt_Rsqr | sqrt => try rewrite derive_pt_sqrt | ?X1 => - let aux := constr:X1 in + let aux := constr:(X1) in match goal with | id:(derive_pt aux pt ?X2 = _),H:(derivable aux) |- _ => try replace (derive_pt aux pt (H pt)) with (derive_pt aux pt X2); diff --git a/theories/ZArith/Int.v b/theories/ZArith/Int.v index d210792f9..32e13d389 100644 --- a/theories/ZArith/Int.v +++ b/theories/ZArith/Int.v @@ -225,11 +225,11 @@ Module MoreInt (Import I:Int). (** [int] to [ExprI] *) Ltac i2ei trm := - match constr:trm with - | 0 => constr:EI0 - | 1 => constr:EI1 - | 2 => constr:EI2 - | 3 => constr:EI3 + match constr:(trm) with + | 0 => constr:(EI0) + | 1 => constr:(EI1) + | 2 => constr:(EI2) + | 3 => constr:(EI3) | ?x + ?y => let ex := i2ei x with ey := i2ei y in constr:(EIadd ex ey) | ?x - ?y => let ex := i2ei x with ey := i2ei y in constr:(EIsub ex ey) | ?x * ?y => let ex := i2ei x with ey := i2ei y in constr:(EImul ex ey) @@ -241,7 +241,7 @@ Module MoreInt (Import I:Int). (** [Z] to [ExprZ] *) with z2ez trm := - match constr:trm with + match constr:(trm) with | (?x + ?y)%Z => let ex := z2ez x with ey := z2ez y in constr:(EZadd ex ey) | (?x - ?y)%Z => let ex := z2ez x with ey := z2ez y in constr:(EZsub ex ey) | (?x * ?y)%Z => let ex := z2ez x with ey := z2ez y in constr:(EZmul ex ey) @@ -254,7 +254,7 @@ Module MoreInt (Import I:Int). (** [Prop] to [ExprP] *) Ltac p2ep trm := - match constr:trm with + match constr:(trm) with | (?x <-> ?y) => let ex := p2ep x with ey := p2ep y in constr:(EPequiv ex ey) | (?x -> ?y) => let ex := p2ep x with ey := p2ep y in constr:(EPimpl ex ey) | (?x /\ ?y) => let ex := p2ep x with ey := p2ep y in constr:(EPand ex ey) diff --git a/theories/ZArith/Zsqrt_compat.v b/theories/ZArith/Zsqrt_compat.v index b80eb4451..f4baba190 100644 --- a/theories/ZArith/Zsqrt_compat.v +++ b/theories/ZArith/Zsqrt_compat.v @@ -30,12 +30,12 @@ Local Open Scope Z_scope. Ltac compute_POS := match goal with | |- context [(Zpos (xI ?X1))] => - match constr:X1 with + match constr:(X1) with | context [1%positive] => fail 1 | _ => rewrite (Pos2Z.inj_xI X1) end | |- context [(Zpos (xO ?X1))] => - match constr:X1 with + match constr:(X1) with | context [1%positive] => fail 1 | _ => rewrite (Pos2Z.inj_xO X1) end |