diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-09-12 11:02:30 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-09-12 11:02:30 +0000 |
| commit | 6fcd224c128ae5e81f4cce9d5de1ac45883cfebf (patch) | |
| tree | 9d5c886b18ca44f3a24de7b58c7dd7ca8bc88eec /kernel/safe_typing.ml | |
| parent | 9248485d71d1c9c1796a22e526e07784493e2008 (diff) | |
Modification mkAppL; abstraction via kind_of_term; changement dans Reduction
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@597 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/safe_typing.ml')
| -rw-r--r-- | kernel/safe_typing.ml | 15 |
1 files changed, 3 insertions, 12 deletions
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index e0c951c22..5c1493e2a 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -94,8 +94,9 @@ let rec execute mf env cstr = | IsAppL (f,args) -> let (j,cst1) = execute mf env f in - let (jl,cst2) = execute_list mf env args in - let (j,cst3) = apply_rel_list env Evd.empty mf.nocheck jl j in + let (jl,cst2) = execute_array mf env args in + let (j,cst3) = + apply_rel_list env Evd.empty mf.nocheck (Array.to_list jl) j in let cst = Constraint.union cst1 (Constraint.union cst2 cst3) in (j, cst) @@ -205,16 +206,6 @@ let unsafe_infer_type env constr = let type_of env c = let (j,_) = safe_infer env c in nf_betaiota env Evd.empty (body_of_type j.uj_type) -(* obsolètes -let type_of_type env c = - let tt = safe_infer_type env c in DOP0 (Sort (level_of_type tt.typ) - -let unsafe_type_of env c = - let (j,_) = unsafe_infer env c in nf_betaiota env Evd.empty j.uj_type - -let unsafe_type_of_type env c = - let tt = unsafe_infer_type env c in DOP0 (Sort tt.typ) -*) (* Typing of several terms. *) let safe_infer_l env cl = |