diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-05-22 11:38:05 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-05-22 11:38:05 +0000 |
| commit | ad103001f8a1eb89f7bec07a0bdecaf19f129c73 (patch) | |
| tree | 5ebc54032ccaf575544da12a05040d2716998464 /Makefile.common | |
| parent | c941fc98f9a707b2a81eb3a1b36d1f497632b04b (diff) | |
QRewrite is now obsolete. It was containing manual ltac stuff
for helping rewriting under Quantifiers and binders, but Matthieu's
setoid rewrite now has the same kind of capabilities by default.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10966 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'Makefile.common')
| -rw-r--r-- | Makefile.common | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/Makefile.common b/Makefile.common index d82137309..c7b7559e9 100644 --- a/Makefile.common +++ b/Makefile.common @@ -651,7 +651,7 @@ REALSVO:=$(REALSBASEVO) $(REALS_$(REALS)) ALLREALS:=$(REALSBASEVO) $(REALS_all) NUMBERSCOMMONVO:=$(addprefix theories/Numbers/, \ - QRewrite.vo NumPrelude.vo BigNumPrelude.vo ) + NumPrelude.vo BigNumPrelude.vo ) CYCLICABSTRACTVO:=$(addprefix theories/Numbers/Cyclic/Abstract/, \ CyclicAxioms.vo NZCyclic.vo ) |