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

2 files changed, 13 insertions, 13 deletions

diff --git a/kernel/environ.ml b/kernel/environ.ml
index 4471d5b87..16284de7b 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -9,7 +9,6 @@ open Univ
 open Generic
 open Term
 open Constant
-open Inductive
 open Abstraction
 
 (* The type of environments. *)
@@ -123,11 +122,6 @@ let lookup_constant sp env =
 let lookup_mind sp env =
   Spmap.find sp env.env_globals.env_inductives
 
-let lookup_mind_specif ((sp,tyi),args) env =
-  let mib = lookup_mind sp env in
-  { mis_sp = sp; mis_mib = mib; mis_tyi = tyi; mis_args = args;
-    mis_mip = mind_nth_type_packet mib tyi }
-
 let lookup_abst sp env =
   Spmap.find sp env.env_globals.env_abstractions
 
@@ -193,12 +187,13 @@ let named_hd env a = function
   | Anonymous -> Name (id_of_string (hdchar env a)) 
   | x         -> x
 
-let prod_name env (n,a,b) = mkProd (named_hd env a n) a b
+let prod_name   env (n,a,b) = mkProd (named_hd env a n) a b
 let lambda_name env (n,a,b) = mkLambda (named_hd env a n) a b
 
-let it_prod_name env = List.fold_left (fun c (n,t) ->prod_name env (n,t,c)) 
+let it_prod_name   env = List.fold_left (fun c (n,t) ->prod_name env (n,t,c)) 
 let it_lambda_name env = List.fold_left (fun c (n,t) ->lambda_name env (n,t,c))
 
+let prod_create   env (a,b) = mkProd (named_hd env a Anonymous) a b
 let lambda_create env (a,b) =  mkLambda (named_hd env a Anonymous) a b
 
 (* Abstractions. *)
diff --git a/kernel/environ.mli b/kernel/environ.mli
index 1d3dcd4c1..720ff16dc 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