aboutsummaryrefslogtreecommitdiff
path: root/Makefile
diff options
context:
space:
mode:
authorbarras2004-09-03 17:14:02 +0000
committerbarras2004-09-03 17:14:02 +0000
commit85fb5f33b1cac28e1fe4f00741c66f6f58109f84 (patch)
tree4913998a925cb148c74a607bf7523ae1d28853ce /Makefile
parent31ebb89fe48efe92786b1cddc3ba62e7dfc4e739 (diff)
premiere reorganisation de l\'unification
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6057 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'Makefile')
-rw-r--r--Makefile10
1 files changed, 6 insertions, 4 deletions
diff --git a/Makefile b/Makefile
index 5af7d0b2e5..48d4b551d2 100644
--- a/Makefile
+++ b/Makefile
@@ -131,14 +131,15 @@ LIBRARY=\
library/decl_kinds.cmo library/dischargedhypsmap.cmo library/goptions.cmo
PRETYPING=\
- pretyping/termops.cmo pretyping/evd.cmo pretyping/instantiate.cmo \
+ pretyping/termops.cmo pretyping/evd.cmo \
pretyping/reductionops.cmo pretyping/inductiveops.cmo \
pretyping/rawterm.cmo pretyping/pattern.cmo \
pretyping/detyping.cmo pretyping/retyping.cmo \
pretyping/cbv.cmo pretyping/tacred.cmo \
- pretyping/pretype_errors.cmo pretyping/typing.cmo \
+ pretyping/pretype_errors.cmo \
pretyping/classops.cmo pretyping/recordops.cmo pretyping/indrec.cmo \
- pretyping/evarutil.cmo pretyping/evarconv.cmo \
+ pretyping/evarutil.cmo pretyping/typing.cmo \
+ pretyping/unification.cmo pretyping/evarconv.cmo \
pretyping/coercion.cmo pretyping/cases.cmo pretyping/pretyping.cmo \
pretyping/matching.cmo
@@ -175,7 +176,8 @@ PROOFS=\
proofs/tacexpr.cmo proofs/proof_type.cmo \
proofs/proof_trees.cmo proofs/logic.cmo \
proofs/refiner.cmo proofs/evar_refiner.cmo proofs/tacmach.cmo \
- proofs/clenv.cmo proofs/pfedit.cmo proofs/tactic_debug.cmo
+ proofs/clenv.cmo proofs/pfedit.cmo proofs/tactic_debug.cmo \
+ proofs/clenvtac.cmo
TACTICS=\
tactics/dn.cmo tactics/termdn.cmo tactics/btermdn.cmo \