From 85fb5f33b1cac28e1fe4f00741c66f6f58109f84 Mon Sep 17 00:00:00 2001
From: barras
Date: Fri, 3 Sep 2004 17:14:02 +0000
Subject: premiere reorganisation de l\'unification

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6057 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 Makefile | 10 ++++++----
 1 file changed, 6 insertions(+), 4 deletions(-)

(limited to 'Makefile')

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 \
-- 
cgit v1.2.3