aboutsummaryrefslogtreecommitdiffhomepage
path: root/Makefile
diff options
context:
space:
mode:
authorGravatar clrenard <clrenard@85f007b7-540e-0410-9357-904b9bb8a0f7>2001-11-12 15:56:10 +0000
committerGravatar clrenard <clrenard@85f007b7-540e-0410-9357-904b9bb8a0f7>2001-11-12 15:56:10 +0000
commitecb17841e955ca888010d72876381a86cdcf09ad (patch)
tree4c6c24f6ce5a8221f8632fceb0f6717948cdca8d /Makefile
parent2f611e10fb3dc42fc00d80b1e087fa33f6fc846e (diff)
Suppression des stamps et donc des *_constraints
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2186 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'Makefile')
-rw-r--r--Makefile4
1 files changed, 2 insertions, 2 deletions
diff --git a/Makefile b/Makefile
index f34fe0d31..45b135ab4 100644
--- a/Makefile
+++ b/Makefile
@@ -70,7 +70,7 @@ CONFIG=config/coq_config.cmo
LIBREP=lib/pp_control.cmo lib/pp.cmo lib/util.cmo \
lib/hashcons.cmo lib/dyn.cmo lib/system.cmo lib/options.cmo \
- lib/bstack.cmo lib/edit.cmo lib/stamps.cmo lib/gset.cmo lib/gmap.cmo \
+ lib/bstack.cmo lib/edit.cmo lib/gset.cmo lib/gmap.cmo \
lib/tlm.cmo lib/bij.cmo lib/gmapl.cmo lib/profile.cmo lib/explore.cmo \
lib/predicate.cmo # Rem: Cygwin already uses variable LIB
@@ -183,7 +183,7 @@ PARSERREQUIRES=config/coq_config.cmo lib/pp_control.cmo lib/pp.cmo \
parsing/termast.cmo \
parsing/astterm.cmo \
parsing/egrammar.cmo parsing/esyntax.cmo toplevel/metasyntax.cmo \
- parsing/printer.cmo lib/stamps.cmo pretyping/typing.cmo \
+ parsing/printer.cmo pretyping/typing.cmo \
proofs/proof_trees.cmo proofs/logic.cmo proofs/refiner.cmo \
proofs/evar_refiner.cmo proofs/tacmach.cmo toplevel/himsg.cmo \
parsing/g_natsyntax.cmo parsing/g_zsyntax.cmo parsing/g_rsyntax.cmo \