From da2de106fc4efdb7a642fd133d8f137dcd526136 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Thu, 18 May 2000 08:17:36 +0000
Subject: Restructuration des outils pour les inductifs. - Les déclarations
 (mutual_inductive_packet et mutual_inductive_body),   utilisisées dans
 Environ vont dans Constant - Instantiations du context local (mind_specif),
 instantiation des   paramètres globaux (inductive_family) et instantiation
 complète   (inductive_type, nouveau nom de inductive_summary) vont dans  
 Inductive qui est déplacé après réduction - Certaines fonctions de Typeops et
 celle traitant des inductifs dans Reduction   et Instantiate sont regroupées
 dans Inductive"

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

(limited to 'Makefile')

diff --git a/Makefile b/Makefile
index 6a87ca40de..a706052783 100644
--- a/Makefile
+++ b/Makefile
@@ -65,9 +65,9 @@ LIB=lib/pp_control.cmo lib/pp.cmo lib/util.cmo \
 
 KERNEL=kernel/names.cmo kernel/generic.cmo kernel/univ.cmo kernel/term.cmo \
        kernel/sign.cmo kernel/constant.cmo \
-       kernel/inductive.cmo kernel/sosub.cmo kernel/abstraction.cmo \
+       kernel/sosub.cmo kernel/abstraction.cmo \
        kernel/environ.cmo kernel/evd.cmo kernel/instantiate.cmo \
-       kernel/closure.cmo kernel/reduction.cmo \
+       kernel/closure.cmo kernel/reduction.cmo kernel/inductive.cmo\
        kernel/type_errors.cmo kernel/typeops.cmo kernel/indtypes.cmo \
        kernel/safe_typing.cmo
 
-- 
cgit v1.2.3