From b71bb95005c9a9db0393bcafc2d43383335c69bf Mon Sep 17 00:00:00 2001
From: herbelin
Date: Thu, 18 May 2000 08:11:44 +0000
Subject: Centralisation prod_name and co dans Environ; mkLambda_string dans
 Term Effets de bords suite à la restructuration des inductives (cf Inductive)

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

(limited to 'kernel/environ.mli')

diff --git a/kernel/environ.mli b/kernel/environ.mli
index 1d3dcd4c14..720ff16dc5 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -5,7 +5,6 @@
 open Names
 open Term
 open Constant
-open Inductive
 open Abstraction
 open Univ
 open Sign
@@ -46,7 +45,6 @@ val lookup_var : identifier -> env -> name * typed_type
 val lookup_rel : int -> env -> name * typed_type
 val lookup_constant : section_path -> env -> constant_body
 val lookup_mind : section_path -> env -> mutual_inductive_body
-val lookup_mind_specif : inductive -> env -> mind_specif
 
 val id_of_global : env -> sorts oper -> identifier
 
@@ -57,18 +55,25 @@ val id_of_name_using_hdchar : env -> constr -> name -> identifier
 
 val named_hd : env -> constr -> name -> name
 
-(* The following functions build product or abstraction and create
-   names using [named_hd] for unnamed binders *)
+(* [lambda_name env (na,t,c)] builds [[[x:t]c] where [x] is created
+   using [named_hd] if [na] is [Anonymous]; [prod_name env (na,t,c)]
+   works similarly but build a product; for [it_lambda_name env c
+   sign] and [it_prod_name env c sign], more recent types should come
+   first in [sign]; none of these functions substitute named
+   variables in [c] by de Bruijn indices *)
 
 val lambda_name : env -> name * constr * constr -> constr
 val prod_name : env -> name * constr * constr -> constr
+
 val it_lambda_name : env -> constr -> (name * constr) list -> constr
 val it_prod_name : env -> constr -> (name * constr) list -> constr
 
 (* [lambda_create env (t,c)] builds [[x:t]c] where [x] is a name built
-   from [t] *)
+   from [t]; [prod_create env (t,c)] builds [(x:t)c] where [x] is a
+   name built from [t] *)
 
 val lambda_create : env -> constr * constr -> constr
+val prod_create : env -> constr * constr -> constr
 
 
 val translucent_abst : env -> constr -> bool
-- 
cgit v1.2.3