aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorherbelin2004-01-21 17:33:50 +0000
committerherbelin2004-01-21 17:33:50 +0000
commite17ed8ec9a03ab8a6ffd63a1bbe8b7b3bcaec3e1 (patch)
treecc267664dd09a99ac45827baf0e1ce1a8d21a674
parent2d64a3c37c204e67548827a11027890ec1f042bf (diff)
Deplacement lexer pour dependance dans constrintern
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5226 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r--Makefile4
1 files changed, 2 insertions, 2 deletions
diff --git a/Makefile b/Makefile
index 97d8141cf2..4c72816449 100644
--- a/Makefile
+++ b/Makefile
@@ -134,14 +134,14 @@ PRETYPING=\
pretyping/matching.cmo
INTERP=\
- interp/topconstr.cmo interp/ppextend.cmo interp/symbols.cmo \
+ parsing/lexer.cmo interp/topconstr.cmo interp/ppextend.cmo interp/symbols.cmo \
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
PARSING=\
- parsing/lexer.cmo parsing/coqast.cmo parsing/ast.cmo \
+ parsing/coqast.cmo parsing/ast.cmo \
parsing/termast.cmo parsing/extend.cmo parsing/esyntax.cmo \
parsing/pcoq.cmo parsing/egrammar.cmo \
parsing/ppconstr.cmo translate/ppconstrnew.cmo parsing/printer.cmo \