From 693d398b5e4e55a916bbdaa8e4c23c83d9dbcef7 Mon Sep 17 00:00:00 2001
From: notin
Date: Wed, 25 Jun 2008 18:19:21 +0000
Subject: Création du fichier dumpglob.ml, qui rassemble les fonctions de
 globalisation (add_glob* et dump_*)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11177 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 Makefile.common | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'Makefile.common')

diff --git a/Makefile.common b/Makefile.common
index f31b60a58b..c0584b29c2 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -172,7 +172,7 @@ PRETYPING:=\
 
 INTERP:=\
   parsing/lexer.cmo interp/topconstr.cmo interp/ppextend.cmo \
-  interp/notation.cmo \
+  interp/notation.cmo interp/dumpglob.cmo \
   interp/genarg.cmo interp/syntax_def.cmo interp/reserve.cmo \
   library/impargs.cmo interp/implicit_quantifiers.cmo interp/constrintern.cmo \
   interp/modintern.cmo interp/constrextern.cmo interp/coqlib.cmo \
@@ -509,7 +509,7 @@ PRINTERSCMO:=\
   pretyping/unification.cmo pretyping/cases.cmo \
   pretyping/pretyping.cmo pretyping/clenv.cmo pretyping/pattern.cmo \
   parsing/lexer.cmo interp/ppextend.cmo interp/genarg.cmo \
-  interp/topconstr.cmo interp/notation.cmo interp/reserve.cmo		\
+  interp/topconstr.cmo interp/notation.cmo  interp/dumpglob.cmo interp/reserve.cmo		\
   library/impargs.cmo interp/constrextern.cmo \
   interp/syntax_def.cmo interp/implicit_quantifiers.cmo  interp/constrintern.cmo \
   proofs/proof_trees.cmo proofs/logic.cmo proofs/refiner.cmo \
-- 
cgit v1.2.3