aboutsummaryrefslogtreecommitdiff
path: root/Makefile
diff options
context:
space:
mode:
authormsozeau2006-03-13 17:38:17 +0000
committermsozeau2006-03-13 17:38:17 +0000
commitdb6c97df4dde8b1ccb2e5b314a4747f66fd524c1 (patch)
tree39ba546322e7f3d4bd4cc9d58260d3f1b4114bd5 /Makefile
parentd9cc734c4cd2a75a303cc08c3df0973077099ab1 (diff)
Update of Subtac contrib. Add {wf n R} as an alternative to {struct n}.
May cause make world to fail because of dependency problems, make depend clean world should fix that (hopefully). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8624 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'Makefile')
-rw-r--r--Makefile3
1 files changed, 3 insertions, 0 deletions
diff --git a/Makefile b/Makefile
index 0d2c5abe31..6edd5ca47d 100644
--- a/Makefile
+++ b/Makefile
@@ -299,6 +299,9 @@ SUBTACCMO=\
contrib/subtac/subtac_errors.cmo \
contrib/subtac/subtac_coercion.cmo \
contrib/subtac/interp.cmo \
+ contrib/subtac/interp_fixpoint.cmo \
+ contrib/subtac/subtac_command.cmo \
+ contrib/subtac/subtac.cmo \
contrib/subtac/sparser.cmo