diff options
Diffstat (limited to 'contrib/setoid_ring')
-rw-r--r-- | contrib/setoid_ring/Field_tac.v | 24 | ||||
-rw-r--r-- | contrib/setoid_ring/Ring_tac.v | 24 | ||||
-rw-r--r-- | contrib/setoid_ring/Ring_theory.v | 2 | ||||
-rw-r--r-- | contrib/setoid_ring/newring.ml4 | 10 |
4 files changed, 28 insertions, 32 deletions
diff --git a/contrib/setoid_ring/Field_tac.v b/contrib/setoid_ring/Field_tac.v index fc89022fd..cccee6045 100644 --- a/contrib/setoid_ring/Field_tac.v +++ b/contrib/setoid_ring/Field_tac.v @@ -143,12 +143,12 @@ Ltac Field_simplify := Field_simplify_gen ltac:(fun H => rewrite H). Tactic Notation (at level 0) "field_simplify" constr_list(rl) := let G := Get_goal in - field_lookup Field_simplify [] rl [G]. + field_lookup Field_simplify [] rl G. Tactic Notation (at level 0) "field_simplify" "[" constr_list(lH) "]" constr_list(rl) := let G := Get_goal in - field_lookup Field_simplify [lH] rl [G]. + field_lookup Field_simplify [lH] rl G. Tactic Notation "field_simplify" constr_list(rl) "in" hyp(H):= let G := Get_goal in @@ -156,7 +156,7 @@ Tactic Notation "field_simplify" constr_list(rl) "in" hyp(H):= let g := fresh "goal" in set (g:= G); generalize H;clear H; - field_lookup Field_simplify [] rl [t]; + field_lookup Field_simplify [] rl t; intro H; unfold g;clear g. @@ -167,7 +167,7 @@ Tactic Notation "field_simplify" let g := fresh "goal" in set (g:= G); generalize H;clear H; - field_lookup Field_simplify [lH] rl [t]; + field_lookup Field_simplify [lH] rl t; intro H; unfold g;clear g. @@ -178,12 +178,12 @@ Ltac Field_simplify_in hyp:= Tactic Notation (at level 0) "field_simplify" constr_list(rl) "in" hyp(h) := let t := type of h in - field_lookup (Field_simplify_in h) [] rl [t]. + field_lookup (Field_simplify_in h) [] rl t. Tactic Notation (at level 0) "field_simplify" "[" constr_list(lH) "]" constr_list(rl) "in" hyp(h) := let t := type of h in - field_lookup (Field_simplify_in h) [lH] rl [t]. + field_lookup (Field_simplify_in h) [lH] rl t. *) (** Generic tactic for solving equations *) @@ -242,11 +242,11 @@ Ltac FIELD := Tactic Notation (at level 0) "field" := let G := Get_goal in - field_lookup FIELD [] [G]. + field_lookup FIELD [] G. Tactic Notation (at level 0) "field" "[" constr_list(lH) "]" := let G := Get_goal in - field_lookup FIELD [lH] [G]. + field_lookup FIELD [lH] G. (* transforms a field equation to an equivalent (simplified) ring equation, and leaves non-zero conditions to be proved (field_simplify_eq) *) @@ -260,11 +260,11 @@ Ltac FIELD_SIMPL := Tactic Notation (at level 0) "field_simplify_eq" := let G := Get_goal in - field_lookup FIELD_SIMPL [] [G]. + field_lookup FIELD_SIMPL [] G. Tactic Notation (at level 0) "field_simplify_eq" "[" constr_list(lH) "]" := let G := Get_goal in - field_lookup FIELD_SIMPL [lH] [G]. + field_lookup FIELD_SIMPL [lH] G. (* Same as FIELD_SIMPL but in hypothesis *) @@ -323,7 +323,7 @@ Ltac FIELD_SIMPL_EQ := Tactic Notation (at level 0) "field_simplify_eq" "in" hyp(H) := let t := type of H in generalize H; - field_lookup FIELD_SIMPL_EQ [] [t]; + field_lookup FIELD_SIMPL_EQ [] t; [ try exact I | clear H;intro H]. @@ -332,7 +332,7 @@ Tactic Notation (at level 0) "field_simplify_eq" "[" constr_list(lH) "]" "in" hyp(H) := let t := type of H in generalize H; - field_lookup FIELD_SIMPL_EQ [lH] [t]; + field_lookup FIELD_SIMPL_EQ [lH] t; [ try exact I |clear H;intro H]. diff --git a/contrib/setoid_ring/Ring_tac.v b/contrib/setoid_ring/Ring_tac.v index d5fc5f348..46d106d37 100644 --- a/contrib/setoid_ring/Ring_tac.v +++ b/contrib/setoid_ring/Ring_tac.v @@ -250,11 +250,11 @@ Ltac Get_goal := match goal with [|- ?G] => G end. Tactic Notation (at level 0) "ring" := let G := Get_goal in - ring_lookup Ring_gen [] [G]. + ring_lookup Ring_gen [] G. Tactic Notation (at level 0) "ring" "[" constr_list(lH) "]" := let G := Get_goal in - ring_lookup Ring_gen [lH] [G]. + ring_lookup Ring_gen [lH] G. (* Simplification *) @@ -281,12 +281,12 @@ Ltac Ring_simplify := Ring_simplify_gen ltac:(fun H => rewrite H). Tactic Notation (at level 0) "ring_simplify" constr_list(rl) := let G := Get_goal in - ring_lookup Ring_simplify [] rl [G]. + ring_lookup Ring_simplify [] rl G. Tactic Notation (at level 0) "ring_simplify" "[" constr_list(lH) "]" constr_list(rl) := let G := Get_goal in - ring_lookup Ring_simplify [lH] rl [G]. + ring_lookup Ring_simplify [lH] rl G. (* MON DIEU QUE C'EST MOCHE !!!!!!!!!!!!! *) @@ -296,7 +296,7 @@ Tactic Notation "ring_simplify" constr_list(rl) "in" hyp(H):= let g := fresh "goal" in set (g:= G); generalize H;clear H; - ring_lookup Ring_simplify [] rl [t]; + ring_lookup Ring_simplify [] rl t; intro H; unfold g;clear g. @@ -307,13 +307,13 @@ Tactic Notation let g := fresh "goal" in set (g:= G); generalize H;clear H; - ring_lookup Ring_simplify [lH] rl [t]; + ring_lookup Ring_simplify [lH] rl t; intro H; unfold g;clear g. -(* LE RESTE MARCHE PAS DOMAGE ..... *) +(* LE RESTE MARCHE PAS DOMMAGE ..... *) @@ -343,11 +343,11 @@ Ltac Ring_simplify_in hyp:= Ring_simplify_gen ltac:(fun H => rewrite H in hyp). Tactic Notation (at level 0) "ring_simplify" "[" constr_list(lH) "]" constr_list(rl) := - match goal with [|- ?G] => ring_lookup Ring_simplify [lH] rl [G] end. + match goal with [|- ?G] => ring_lookup Ring_simplify [lH] rl G end. Tactic Notation (at level 0) "ring_simplify" constr_list(rl) := - match goal with [|- ?G] => ring_lookup Ring_simplify [] rl [G] end. + match goal with [|- ?G] => ring_lookup Ring_simplify [] rl G end. Tactic Notation (at level 0) "ring_simplify" "[" constr_list(lH) "]" constr_list(rl) "in" hyp(h):= @@ -357,7 +357,7 @@ Tactic Notation (at level 0) pre(); Ring_norm_gen ltac:(fun EQ => rewrite EQ in h) cst_tac pow_tac lemma2 req ring_subst_niter lH rl; post()) - [lH] rl [t]. + [lH] rl t. (* ring_lookup ltac:(Ring_simplify_in h) [lH] rl [t]. NE MARCHE PAS ??? *) Ltac Ring_simpl_in hyp := Ring_norm_gen ltac:(fun H => rewrite H in hyp). @@ -370,7 +370,7 @@ Tactic Notation (at level 0) pre(); Ring_simpl_in h cst_tac pow_tac lemma2 req ring_subst_niter lH rl; post()) - [] rl [t]. + [] rl t. Ltac rw_in H Heq := rewrite Heq in H. @@ -381,7 +381,7 @@ Ltac simpl_in H := pre(); Ring_norm_gen ltac:(fun Heq => rewrite Heq in H) cst_tac pow_tac lemma2 req ring_subst_niter lH rl; post()) - [] [t]. + [] t. *) diff --git a/contrib/setoid_ring/Ring_theory.v b/contrib/setoid_ring/Ring_theory.v index 4c542ffdd..b7876130a 100644 --- a/contrib/setoid_ring/Ring_theory.v +++ b/contrib/setoid_ring/Ring_theory.v @@ -19,8 +19,6 @@ Reserved Notation "x -! y" (at level 50, left associativity). Reserved Notation "x *! y" (at level 40, left associativity). Reserved Notation "-! x" (at level 35, right associativity). -Reserved Notation "[ x ]" (at level 1, no associativity). - Reserved Notation "x ?== y" (at level 70, no associativity). Reserved Notation "x -- y" (at level 50, left associativity). Reserved Notation "x ** y" (at level 40, left associativity). diff --git a/contrib/setoid_ring/newring.ml4 b/contrib/setoid_ring/newring.ml4 index c80b37d91..c3caa403e 100644 --- a/contrib/setoid_ring/newring.ml4 +++ b/contrib/setoid_ring/newring.ml4 @@ -828,9 +828,8 @@ let ring_lookup (f:glob_tactic_expr) lH rl t gl = lemma1;lemma2;pretac;posttac;lH;rl])) gl TACTIC EXTEND ring_lookup -| [ "ring_lookup" tactic(f) "[" constr_list(lH) "]" constr_list(lr) - "[" constr(t) "]" ] -> - [ring_lookup (fst f) lH lr t] +| [ "ring_lookup" tactic0(f) "[" constr_list(lH) "]" ne_constr_list(lrt) ] -> + [ let (t,lr) = list_sep_last lrt in ring_lookup (fst f) lH lr t] END @@ -1163,7 +1162,6 @@ let field_lookup (f:glob_tactic_expr) lH rl t gl = field_simpl_eq_in_ok;cond_ok;pretac;posttac;lH;rl])) gl TACTIC EXTEND field_lookup -| [ "field_lookup" tactic(f) "[" constr_list(lH) "]" constr_list(l) - "[" constr(t) "]" ] -> - [ field_lookup (fst f) lH l t ] +| [ "field_lookup" tactic0(f) "[" constr_list(lH) "]" ne_constr_list(lt) ] -> + [ let (t,l) = list_sep_last lt in field_lookup (fst f) lH l t ] END |