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 /checker/votour.ml | |
| 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 'checker/votour.ml')
0 files changed, 0 insertions, 0 deletions