diff options
| author | filliatr | 1999-11-26 16:09:40 +0000 |
|---|---|---|
| committer | filliatr | 1999-11-26 16:09:40 +0000 |
| commit | 82667b4dc6d4a34708c2b9a14a940e05ea9044f7 (patch) | |
| tree | f992de7a8469f8a8f0c37c771532101562a9e37f /Makefile | |
| parent | 3d4a8fc16cf415643be2a5707248c1858a307023 (diff) | |
module Classops; ajout de fonctions dans Declare en consequence
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@152 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'Makefile')
| -rw-r--r-- | Makefile | 20 |
1 files changed, 18 insertions, 2 deletions
@@ -59,11 +59,15 @@ TACTICS=tactics/dn.cmo tactics/termdn.cmo tactics/btermdn.cmo \ tactics/wcclausenv.cmo tactics/tacticals.cmo \ tactics/tacentries.cmo tactics/hiddentac.cmo tactics/elim.cmo -PRETYPING=pretyping/astterm.cmo +PRETYPING=pretyping/classops.cmo pretyping/recordops.cmo \ + pretyping/evarutil.cmo pretyping/evarconv.cmo \ + pretyping/pretype_errors.cmo pretyping/coercion.cmo \ + pretyping/multcase.cmo pretyping/pretyping.cmo PARSING=parsing/lexer.cmo parsing/coqast.cmo parsing/pcoq.cmo parsing/ast.cmo \ parsing/g_prim.cmo parsing/g_basevernac.cmo parsing/g_vernac.cmo \ - parsing/g_command.cmo parsing/g_tactic.cmo parsing/g_multiple_case.cmo + parsing/g_command.cmo parsing/g_tactic.cmo parsing/g_multiple_case.cmo\ + parsing/printer.cmo parsing/pretty.cmo parsing/astterm.cmo TOPLEVEL=toplevel/himsg.cmo toplevel/errors.cmo toplevel/vernacinterp.cmo \ toplevel/vernac.cmo toplevel/mltop.cmo \ @@ -80,6 +84,14 @@ CMX=$(CMO:.cmo=.cmx) world: minicoq coqtop.byte dev/db_printers.cmo +kernel: $(KERNEL) +library: $(LIBRARY) +proofs: $(PROOFS) +tactics: $(TACTICS) +parsing: $(PARSING) +pretyping: $(PRETYPING) +toplevel: $(TOPLEVEL) + # coqtop coqtop: $(CMX) @@ -215,6 +227,8 @@ archclean:: rm -f proofs/*.cmx proofs/*.[so] rm -f tactics/*.cmx tactics/*.[so] rm -f parsing/*.cmx parsing/*.[so] + rm -f pretyping/*.cmx pretyping/*.[so] + rm -f toplevel/*.cmx toplevel/*.[so] cleanall:: archclean rm -f *~ @@ -226,6 +240,8 @@ cleanall:: archclean rm -f proofs/*.cm[io] proofs/*~ rm -f tactics/*.cm[io] tactics/*~ rm -f parsing/*.cm[io] parsing/*.ppo parsing/*~ + rm -f pretyping/*.cm[io] pretyping/*~ + rm -f toplevel/*.cm[io] toplevel/*~ cleanconfig:: rm -f config/Makefile config/coq_config.ml |