diff options
| author | herbelin | 2000-05-18 08:11:44 +0000 |
|---|---|---|
| committer | herbelin | 2000-05-18 08:11:44 +0000 |
| commit | b71bb95005c9a9db0393bcafc2d43383335c69bf (patch) | |
| tree | 7b48b3b855c3a36cd6443f43d7c51703b4c44074 /kernel/environ.ml | |
| parent | 5bf752c55c86445995c3eae0b952c72b7b8c8a9a (diff) | |
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
Diffstat (limited to 'kernel/environ.ml')
| -rw-r--r-- | kernel/environ.ml | 11 |
1 files changed, 3 insertions, 8 deletions
diff --git a/kernel/environ.ml b/kernel/environ.ml index 4471d5b873..16284de7b2 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. *) |