diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-08-13 16:13:32 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-08-13 16:13:32 +0000 |
| commit | 5c668276b37f09077231c314b03254df6dce3c48 (patch) | |
| tree | b8bb01cd33a1bf16d9270359dbac796a223a4f32 /kernel | |
| parent | a3848b0a10064fb7e206a503ac8b829cb9ce4666 (diff) | |
Renoncement
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2962 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/environ.ml | 2 | ||||
| -rw-r--r-- | kernel/term.ml | 12 | ||||
| -rw-r--r-- | kernel/typeops.ml | 4 |
3 files changed, 9 insertions, 9 deletions
diff --git a/kernel/environ.ml b/kernel/environ.ml index d32d232fa..6449c183f 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -224,7 +224,7 @@ let keep_hyps env needed = | None -> Idset.empty | Some c -> global_vars_set env c in Idset.union - (global_vars_set env (body_of_type t)) + (global_vars_set env t) (Idset.union globc need) else need) ~init:needed diff --git a/kernel/term.ml b/kernel/term.ml index 0c5dc2a54..da8c3062a 100644 --- a/kernel/term.ml +++ b/kernel/term.ml @@ -891,8 +891,8 @@ let mkProd_or_LetIn (na,body,t) c = let mkNamedProd_or_LetIn (id,body,t) c = match body with - | None -> mkNamedProd id (body_of_type t) c - | Some b -> mkNamedLetIn id b (body_of_type t) c + | None -> mkNamedProd id t c + | Some b -> mkNamedLetIn id b t c (* Constructs either [[x:t]c] or [[x=b:t]c] *) let mkLambda_or_LetIn (na,body,t) c = @@ -902,18 +902,18 @@ let mkLambda_or_LetIn (na,body,t) c = let mkNamedLambda_or_LetIn (id,body,t) c = match body with - | None -> mkNamedLambda id (body_of_type t) c - | Some b -> mkNamedLetIn id b (body_of_type t) c + | None -> mkNamedLambda id t c + | Some b -> mkNamedLetIn id b t c (* Constructs either [(x:t)c] or [c] where [x] is replaced by [b] *) let mkProd_wo_LetIn (na,body,t) c = match body with - | None -> mkProd (na, body_of_type t, c) + | None -> mkProd (na, t, c) | Some b -> subst1 b c let mkNamedProd_wo_LetIn (id,body,t) c = match body with - | None -> mkNamedProd id (body_of_type t) c + | None -> mkNamedProd id t c | Some b -> subst1 b (subst_var id c) (* non-dependent product t1 -> t2 *) diff --git a/kernel/typeops.ml b/kernel/typeops.ml index 29b09dde1..88de140df 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -177,7 +177,7 @@ let judge_of_apply env funj argjv = apply_rec (n+1) (subst1 hj.uj_val c2) cst' restjl with NotConvertible -> error_cant_apply_bad_type env - (n,c1,body_of_type hj.uj_type) + (n,c1, hj.uj_type) funj argjv) | _ -> @@ -312,7 +312,7 @@ let type_fixpoint env lna lar vdefj = try conv_leq_vecti env (Array.map (fun j -> body_of_type j.uj_type) vdefj) - (Array.map (fun ty -> lift lt (body_of_type ty)) lar) + (Array.map (fun ty -> lift lt ty) lar) with NotConvertibleVect i -> error_ill_typed_rec_body env i lna vdefj lar |