diff options
| author | msozeau | 2009-04-13 23:07:54 +0000 |
|---|---|---|
| committer | msozeau | 2009-04-13 23:07:54 +0000 |
| commit | 0e608025f45c9ffc2573c72e5c23bc183e3ab0b3 (patch) | |
| tree | 69d66976f12d7bc9f46e1ba681fa9401a8515226 /dev | |
| parent | e2655d38d11b072da0e5f4d40b05adbea73c8b8d (diff) | |
Rewrite of setoid_rewrite to modularize it based on proof-producing
strategies (à la ELAN).
Now setoid_rewrite is just one strategy and autorewrite is a
more elaborate one. Any kind of traversals can be defined, strategies
can be composed etc... in ML. An incomplete (no fix) language extension
for specifying them in Ltac is there too.
On a typical autorewrite-with-setoids usage, proof production time is
divided by 2 and proof size by 10.
Fix some admitted proofs and buggy patterns in Classes.Morphisms as
well.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12081 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions