diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-08-22 10:07:54 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-08-22 10:07:54 +0000 |
| commit | 1f3331bd4ff9fd562d534554185db2b6c4cc9e78 (patch) | |
| tree | c33feca82cea5bc7a2b0301d69b47daee43ab2fd /plugins/setoid_ring/Field_tac.v | |
| parent | 39c502b33f823d06fafde0d1480ddafc82a89da4 (diff) | |
Field_theory : faster and nicer proofs + nice notations.
This file should compile now twice as fast as earlier.
A large part of this speedup comes from swithching to
proofs without "auto" (and also improving them quite a lot).
Nicer lemma statements thanks to notations and
separate scopes (%ring, %coef, %poly).
The Field_correct lemma lost some args (sign_theory ...)
during the refactoring. After inspection, this looks legitimate,
so I've hack the field tactic accordingly. The args were there
probably due to some intuition or similar interfering with local
vars.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16721 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins/setoid_ring/Field_tac.v')
| -rw-r--r-- | plugins/setoid_ring/Field_tac.v | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/plugins/setoid_ring/Field_tac.v b/plugins/setoid_ring/Field_tac.v index 8ac952c04..c46e7a933 100644 --- a/plugins/setoid_ring/Field_tac.v +++ b/plugins/setoid_ring/Field_tac.v @@ -542,10 +542,9 @@ Ltac field_lemmas set ext inv_m fspec pspec sspec dspec rk := let field_ok2 := constr:(field_ok1 _ _ _ pp_spec) in match s_spec with | mkhypo ?ss_spec => - let field_ok3 := constr:(field_ok2 _ ss_spec) in match d_spec with | mkhypo ?dd_spec => - let field_ok := constr:(field_ok3 _ dd_spec) in + let field_ok := constr:(field_ok2 _ dd_spec) in let mk_lemma lemma := constr:(lemma _ _ _ _ _ _ _ _ _ _ set ext_r inv_m afth |