aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-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 \