diff options
| author |  ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-07-19 14:59:28 +0000 |
|---|---|---|
| committer | ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-07-19 14:59:28 +0000 |
| commit | 476d70df227f6880e7fce29c30f2158f83ce05b9 (patch) | |
| tree | 246460f3b622baaa61b23e48e7d367f7f0c18bab | |
| parent | f90854e62a8025eb1477c743dfef64a66f7da535 (diff) | |
Getting rid of the undocumented [complete] tactic, which was
redundant with [solve]. The AST node still exists in Ltac, because
this is used by the [assert ... by ...] tactical. Fixes #2847.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15625 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | parsing/g_ltac.ml4 | 1 | ||||
| -rw-r--r-- | plugins/setoid_ring/Field_theory.v | 6 | ||||
| -rw-r--r-- | printing/pptactic.ml | 2 |
3 files changed, 4 insertions, 5 deletions
diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4 index 5da6ddf3d..663578429 100644 --- a/parsing/g_ltac.ml4 +++ b/parsing/g_ltac.ml4 @@ -81,7 +81,6 @@ GEXTEND Gram TacFirst l | IDENT "solve" ; "["; l = LIST0 tactic_expr SEP "|"; "]" -> TacSolve l - | IDENT "complete" ; ta = tactic_expr -> TacComplete ta | IDENT "idtac"; l = LIST0 message_token -> TacId l | IDENT "fail"; n = [ n = int_or_var -> n | -> fail_default_value ]; l = LIST0 message_token -> TacFail (n,l) diff --git a/plugins/setoid_ring/Field_theory.v b/plugins/setoid_ring/Field_theory.v index bd9622e52..0bd806c15 100644 --- a/plugins/setoid_ring/Field_theory.v +++ b/plugins/setoid_ring/Field_theory.v @@ -201,7 +201,7 @@ Theorem rdiv2: r1 / r2 + r3 / r4 == (r1 * r4 + r3 * r2) / (r2 * r4). Proof. intros r1 r2 r3 r4 H H0. -assert (~ r2 * r4 == 0) by complete (apply field_is_integral_domain; trivial). +assert (~ r2 * r4 == 0) by (apply field_is_integral_domain; trivial). apply rmul_reg_l with (r2 * r4); trivial. rewrite rdiv_simpl; trivial. rewrite (ARdistr_r Rsth Reqe ARth). @@ -223,7 +223,7 @@ assert (HH1: ~ r2 == 0) by (intros HH; case H; rewrite HH; ring). assert (HH2: ~ r5 == 0) by (intros HH; case H; rewrite HH; ring). assert (HH3: ~ r4 == 0) by (intros HH; case H0; rewrite HH; ring). assert (HH4: ~ r2 * (r4 * r5) == 0) - by complete (repeat apply field_is_integral_domain; trivial). + by (repeat apply field_is_integral_domain; trivial). apply rmul_reg_l with (r2 * (r4 * r5)); trivial. rewrite rdiv_simpl; trivial. rewrite (ARdistr_r Rsth Reqe ARth). @@ -295,7 +295,7 @@ Hint Resolve rdiv6 . (r1 / r2) * (r3 / r4) == (r1 * r3) / (r2 * r4). Proof. intros r1 r2 r3 r4 H H0. -assert (~ r2 * r4 == 0) by complete (apply field_is_integral_domain; trivial). +assert (~ r2 * r4 == 0) by (apply field_is_integral_domain; trivial). apply rmul_reg_l with (r2 * r4); trivial. rewrite rdiv_simpl; trivial. transitivity (r2 * (r1 / r2) * (r4 * (r3 / r4))); [ ring | idtac ]. diff --git a/printing/pptactic.ml b/printing/pptactic.ml index f89877e00..6d921f85f 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -916,7 +916,7 @@ let rec pr_tac inherited tac = | TacSolve tl -> str "solve" ++ spc () ++ pr_seq_body (pr_tac ltop) tl, llet | TacComplete t -> - str "complete" ++ spc () ++ pr_tac (lcomplete,E) t, lcomplete + pr_tac (lcomplete,E) t, lcomplete | TacId l -> str "idtac" ++ prlist (pr_arg (pr_message_token pr_ident)) l, latom | TacAtom (loc,TacAlias (_,s,l,_)) -> |