From e7d592ada2d681876d2bcf0a45d4267b3746064f Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 14 Feb 2001 15:41:55 +0000
Subject: Mise en place d'un système optionnel de discharge immédiat; prise en
 compte des défs locales dans les arguments des inductifs; nettoyage divers

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1381 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/environ.mli | 1 +
 1 file changed, 1 insertion(+)

(limited to 'kernel/environ.mli')

diff --git a/kernel/environ.mli b/kernel/environ.mli
index 65a2bb671d..eba1e09793 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -140,6 +140,7 @@ val it_mkProd_or_LetIn : constr -> rel_context -> constr
 
 val it_mkNamedLambda_or_LetIn : constr -> named_context -> constr
 val it_mkNamedProd_or_LetIn : constr -> named_context -> constr
+val it_mkNamedProd_wo_LetIn : constr -> named_context -> constr
 
 (* [lambda_create env (t,c)] builds [[x:t]c] where [x] is a name built
    from [t]; [prod_create env (t,c)] builds [(x:t)c] where [x] is a
-- 
cgit v1.2.3