From cf136fb80c1b461b16d733830d8a320e6d03d06b Mon Sep 17 00:00:00 2001
From: vsiles
Date: Fri, 5 Oct 2007 13:02:23 +0000
Subject:  Added the automatic generation of the boolean equality if possible
 and the decidability of the usual equality Major changes:  * andb_prop &
 andb_true_intro have been moved from Bool.v to Datatypes.v  * added 2 files: 
    * toplevel/ind_tables.ml* : tables where the boolean eqs and the        
 decidability proofs are stored     * toplevel/auto_ind_decl.ml* : code of the
 schemes that are automatically         generated from inductives types
 (currently boolean eq & decidability )  * improvement of injection: if the
 decidability have been correctly computed,    injection can now break the
 equalities over dependant pair

How to use:
 Set Equality Scheme. to set the automatic generation of the equality when you
create a new inductive type
 Scheme Equality for I. tries to create the equality for the already declared
type I




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

(limited to 'Makefile.common')

diff --git a/Makefile.common b/Makefile.common
index 08feab44b5..ba911adb07 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -147,6 +147,7 @@ TACTICS:=\
   tactics/evar_tactics.cmo \
   tactics/hiddentac.cmo tactics/elim.cmo \
   tactics/dhyp.cmo tactics/auto.cmo \
+  toplevel/ind_tables.cmo \
   tactics/setoid_replace.cmo tactics/equality.cmo \
   tactics/contradiction.cmo tactics/inv.cmo tactics/leminv.cmo \
   tactics/tacinterp.cmo tactics/autorewrite.cmo \
@@ -155,6 +156,7 @@ TACTICS:=\
 TOPLEVEL:=\
   toplevel/himsg.cmo toplevel/cerrors.cmo toplevel/class.cmo \
   toplevel/vernacexpr.cmo toplevel/metasyntax.cmo \
+  toplevel/auto_ind_decl.cmo \
   toplevel/command.cmo toplevel/record.cmo \
   parsing/ppvernac.cmo \
   toplevel/vernacinterp.cmo toplevel/mltop.cmo \
-- 
cgit v1.2.3