diff options
| author | herbelin | 2001-06-25 11:12:33 +0000 |
|---|---|---|
| committer | herbelin | 2001-06-25 11:12:33 +0000 |
| commit | 54119fc2b8b38690d708aa7967e8a690e42904ae (patch) | |
| tree | a3f87947cf976f325448249e9d36d9d9061840bc /Makefile | |
| parent | a7c192aaf3895e50635a921caee1e3276df1d399 (diff) | |
Découpage de g_tactic.ml4 en 2 (pour satisfaire les contraintes de la compilation native powerpc), le nouveau morceau étant g_ltac.ml4
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1803 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'Makefile')
| -rw-r--r-- | Makefile | 7 |
1 files changed, 4 insertions, 3 deletions
@@ -96,7 +96,7 @@ PARSING=parsing/lexer.cmo parsing/coqast.cmo parsing/pcoq.cmo parsing/ast.cmo \ parsing/termast.cmo parsing/astterm.cmo parsing/coqlib.cmo \ parsing/g_prim.cmo parsing/g_basevernac.cmo \ parsing/g_vernac.cmo parsing/g_proofs.cmo parsing/g_tactic.cmo \ - parsing/g_constr.cmo parsing/g_cases.cmo \ + parsing/g_ltac.cmo parsing/g_constr.cmo parsing/g_cases.cmo \ parsing/extend.cmo parsing/esyntax.cmo \ parsing/printer.cmo parsing/prettyp.cmo parsing/search.cmo \ parsing/egrammar.cmo \ @@ -165,7 +165,7 @@ PARSERREQUIRES=lib/pp_control.cmo lib/pp.cmo \ parsing/pcoq.cmo parsing/ast.cmo \ parsing/g_prim.cmo parsing/g_basevernac.cmo \ parsing/g_vernac.cmo parsing/g_proofs.cmo parsing/g_tactic.cmo \ - parsing/g_constr.cmo parsing/g_cases.cmo \ + parsing/g_ltac.cmo parsing/g_constr.cmo parsing/g_cases.cmo \ parsing/extend.cmo config/coq_config.cmo\ lib/system.cmo lib/bstack.cmo lib/edit.cmo \ library/nametab.cmo kernel/univ.cmo library/lib.cmo kernel/esubst.cmo \ @@ -695,7 +695,8 @@ clean:: ML4FILES +=parsing/g_basevernac.ml4 parsing/g_minicoq.ml4 \ parsing/g_vernac.ml4 parsing/g_proofs.ml4 parsing/g_cases.ml4 \ - parsing/g_constr.ml4 parsing/g_tactic.ml4 parsing/extend.ml4 + parsing/g_constr.ml4 parsing/g_tactic.ml4 parsing/g_ltac.ml4 \ + parsing/extend.ml4 # beforedepend:: $(GRAMMARCMO) |