diff options
| author | herbelin | 1999-12-01 23:13:01 +0000 |
|---|---|---|
| committer | herbelin | 1999-12-01 23:13:01 +0000 |
| commit | f99150300603ce0d87db716efc52fa88967d4460 (patch) | |
| tree | 4a85be13031030ac01659359b032411bfd63a73b /Makefile | |
| parent | 3a49dbf016e1ebf8f8d12ed43fde14c5619ca55e (diff) | |
Intégration du Termast et du Retyping de HH, et modifications connexes
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@185 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'Makefile')
| -rw-r--r-- | Makefile | 14 |
1 files changed, 8 insertions, 6 deletions
@@ -49,16 +49,18 @@ LIBRARY=library/libobject.cmo library/summary.cmo library/lib.cmo \ library/nametab.cmo library/impargs.cmo library/redinfo.cmo \ library/indrec.cmo library/declare.cmo -PRETYPING=pretyping/typing.cmo pretyping/classops.cmo pretyping/recordops.cmo \ - pretyping/evarutil.cmo pretyping/evarconv.cmo \ +PRETYPING=pretyping/retyping.cmo pretyping/typing.cmo \ + 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 + pretyping/cases.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/printer.cmo parsing/pretty.cmo parsing/astterm.cmo \ - parsing/egrammar.cmo + parsing/g_command.cmo parsing/g_tactic.cmo parsing/g_cases.cmo\ + parsing/printer.cmo parsing/pretty.cmo \ + parsing/termast.cmo parsing/astterm.cmo \ + parsing/egrammar.cmo PROOFS=proofs/tacred.cmo \ proofs/proof_trees.cmo proofs/logic.cmo \ |