From f7da904e8702bd144f25fa3a80307a994a39f1d6 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 15 Sep 2000 16:44:52 +0000
Subject: On laisse les LetIn dans les types des constructeurs et des
 éliminations

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

(limited to 'kernel/reduction.mli')

diff --git a/kernel/reduction.mli b/kernel/reduction.mli
index d1a092ae7f..7bb43b0556 100644
--- a/kernel/reduction.mli
+++ b/kernel/reduction.mli
@@ -115,6 +115,8 @@ val splay_arity : env -> 'a evar_map -> constr -> (name * constr) list * sorts
 val sort_of_arity : env -> constr -> sorts
 val decomp_n_prod : 
   env -> 'a evar_map -> int -> constr -> Sign.rel_context * constr
+val splay_prod_assum :
+  env -> 'a evar_map -> constr -> Sign.rel_context * constr
 
 type 'a miota_args = {
   mP      : constr;     (* the result type *)
-- 
cgit v1.2.3