From 2206b405c19940ca4ded2179d371c21fd13f1b6b Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 24 Feb 2015 23:58:56 +0100 Subject: Adding a new folder corresponding to the low-level part of the pretyper together with the tactic monad. The move is not complete yet, because some file candidates for this directory have almost useless dependencies in other ones that should not be moved. --- Makefile.common | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'Makefile.common') diff --git a/Makefile.common b/Makefile.common index 8c2f51467..16782650a 100644 --- a/Makefile.common +++ b/Makefile.common @@ -63,7 +63,7 @@ CSDPCERT:=plugins/micromega/csdpcert$(EXE) CORESRCDIRS:=\ config lib kernel kernel/byterun library \ proofs tactics pretyping interp stm \ - toplevel parsing printing grammar intf + toplevel parsing printing grammar intf engine PLUGINS:=\ omega romega micromega quote \ @@ -161,7 +161,7 @@ BYTERUN:=$(addprefix kernel/byterun/, \ # the libraries directly CORECMA:=lib/clib.cma lib/lib.cma kernel/kernel.cma library/library.cma \ - pretyping/pretyping.cma interp/interp.cma proofs/proofs.cma \ + engine/engine.cma pretyping/pretyping.cma interp/interp.cma proofs/proofs.cma \ parsing/parsing.cma printing/printing.cma tactics/tactics.cma \ stm/stm.cma toplevel/toplevel.cma parsing/highparsing.cma tactics/hightactics.cma @@ -370,7 +370,7 @@ MANPAGES:=man/coq-tex.1 man/coqdep.1 man/gallina.1 \ OCAMLDOCDIR=dev/ocamldoc DOCMLIS=$(wildcard ./lib/*.mli ./intf/*.mli ./kernel/*.mli ./library/*.mli \ - ./pretyping/*.mli ./interp/*.mli printing/*.mli \ + ./engine/*.mli ./pretyping/*.mli ./interp/*.mli printing/*.mli \ ./parsing/*.mli ./proofs/*.mli \ ./tactics/*.mli ./stm/*.mli ./toplevel/*.mli) -- cgit v1.2.3