From f2b9dfdfb72abb3b797bd651a5846a7e7c761847 Mon Sep 17 00:00:00 2001 From: herbelin Date: Thu, 21 Jun 2007 17:01:21 +0000 Subject: Correction de plusieurs bugs de l'export XML (utilisation d'un type de constante par defaut pour les nouveaux types plutot qu'echouer; avertissement plutot qu'echec en cas de foncteur; nommage systematique des LetIn -- p.ex. functional induction engendre des LetIn non nommes --; branchement de la fonction de normalisation de tete evitant CProp sur Closure au lieu de Tacred afin de garantir la f.n. de tete) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9902 85f007b7-540e-0410-9357-904b9bb8a0f7 --- kernel/closure.mli | 6 +----- 1 file changed, 1 insertion(+), 5 deletions(-) (limited to 'kernel') diff --git a/kernel/closure.mli b/kernel/closure.mli index 2a0c1f89e..ea8bccede 100644 --- a/kernel/closure.mli +++ b/kernel/closure.mli @@ -37,11 +37,7 @@ module type RedFlagsSig = sig type reds type red_kind - (* The different kind of reduction *) - (* Const/Var means the reference as argument should be unfolded *) - (* Constbut/Varbut means all references except the ones as argument - of Constbut/Varbut should be unfolded (there may be several such - Constbut/Varbut *) + (* The different kinds of reduction *) val fBETA : red_kind val fDELTA : red_kind val fIOTA : red_kind -- cgit v1.2.3