diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2005-02-18 22:17:50 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2005-02-18 22:17:50 +0000 |
| commit | 7b2a24d0beee17b61281a5c64fca5cf7388479d3 (patch) | |
| tree | 7df42aa9ea5cf3e5ae6066c0aa73673cd67bc19d /Makefile | |
| parent | 8c417a6d32e379d9642d6f2ef144f33d7df4832e (diff) | |
Moving centralised discharge into dispatched discharge_function; required to delay some computation from before to after caching time + various simplifications and uniformisations
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6748 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'Makefile')
| -rw-r--r-- | Makefile | 7 |
1 files changed, 3 insertions, 4 deletions
@@ -161,7 +161,7 @@ INTERP=\ interp/genarg.cmo interp/syntax_def.cmo interp/reserve.cmo \ library/impargs.cmo interp/constrintern.cmo \ interp/modintern.cmo interp/constrextern.cmo interp/coqlib.cmo \ - library/declare.cmo + toplevel/discharge.cmo library/declare.cmo PROOFS=\ proofs/tacexpr.cmo proofs/proof_type.cmo proofs/redexpr.cmo \ @@ -206,9 +206,8 @@ TACTICS=\ TOPLEVEL=\ toplevel/himsg.cmo toplevel/cerrors.cmo toplevel/class.cmo \ toplevel/vernacexpr.cmo toplevel/metasyntax.cmo \ - toplevel/command.cmo \ - toplevel/record.cmo toplevel/recordobj.cmo \ - toplevel/discharge.cmo translate/ppvernacnew.cmo \ + toplevel/command.cmo toplevel/record.cmo \ + translate/ppvernacnew.cmo \ toplevel/vernacinterp.cmo toplevel/mltop.cmo \ toplevel/vernacentries.cmo toplevel/vernac.cmo \ toplevel/line_oriented_parser.cmo toplevel/protectedtoplevel.cmo \ |