diff options
Diffstat (limited to 'kernel')
-rw-r--r-- | kernel/evd.mli | 4 | ||||
-rw-r--r-- | kernel/term.ml | 11 | ||||
-rw-r--r-- | kernel/term.mli | 4 | ||||
-rw-r--r-- | kernel/typeops.mli | 2 | ||||
-rw-r--r-- | kernel/typing.ml | 10 |
5 files changed, 14 insertions, 17 deletions
diff --git a/kernel/evd.mli b/kernel/evd.mli index df80ee72b..62378f921 100644 --- a/kernel/evd.mli +++ b/kernel/evd.mli @@ -10,8 +10,8 @@ open Environ (* The type of mappings for existential variables. The keys are integers and the associated information is a record - containing the type of the evar ([concl]), the signature under which - it was introduced ([hyps]) and its definition ([body]). + containing the type of the evar ([evar_concl]), the environment under which + it was introduced ([evar_env]) and its definition ([evar_body]). [evar_info] is used to add any other kind of information. *) type evar = int diff --git a/kernel/term.ml b/kernel/term.ml index 5d9817fde..4694a75a2 100644 --- a/kernel/term.ml +++ b/kernel/term.ml @@ -131,8 +131,8 @@ let mkLambda x t1 t2 = (DOP2 (Lambda,t1,(DLAM (x,t2)))) let mkNamedLambda name typ c = mkLambda (Name name) typ (subst_var name c) (* If lt = [t1; ...; tn], constructs the application (t1 ... tn) *) -let mkAppL a = DOPN (AppL, a) -let mkAppList l = DOPN (AppL, Array.of_list l) +let mkAppL a = DOPN (AppL, a) +let mkAppList a l = DOPN (AppL, Array.of_list (a::l)) (* Constructs a constant *) (* The array of terms correspond to the variables introduced in the section *) @@ -482,7 +482,7 @@ type kindOfTerm = | IsCast of constr * constr | IsProd of name * constr * constr | IsLambda of name * constr * constr - | IsAppL of constr array + | IsAppL of constr * constr list | IsConst of section_path * constr array | IsAbst of section_path * constr array | IsEvar of int * constr array @@ -509,9 +509,10 @@ let kind_of_term c = | DOP2 (Cast, t1, t2) -> IsCast (t1,t2) | DOP2 (Prod, t1, (DLAM (x,t2))) -> IsProd (x,t1,t2) | DOP2 (Lambda, t1, (DLAM (x,t2))) -> IsLambda (x,t1,t2) - | DOPN (AppL,a) -> IsAppL a + | DOPN (AppL,a) when Array.length a <> 0 -> + IsAppL (a.(0), List.tl (Array.to_list a)) | DOPN (Const sp, a) -> IsConst (sp,a) - | DOPN (Evar sp, a) -> IsEvar (sp,a) + | DOPN (Evar sp, a) -> IsEvar (sp,a) | DOPN (Abst sp, a) -> IsAbst (sp, a) | DOPN (MutInd (sp,i), l) -> IsMutInd (sp,i,l) | DOPN (MutConstruct ((sp,i), j),l) -> IsMutConstruct (sp,i,j,l) diff --git a/kernel/term.mli b/kernel/term.mli index 1fa03507f..511361241 100644 --- a/kernel/term.mli +++ b/kernel/term.mli @@ -75,7 +75,7 @@ type kindOfTerm = | IsCast of constr * constr | IsProd of name * constr * constr | IsLambda of name * constr * constr - | IsAppL of constr array + | IsAppL of constr * constr list | IsConst of section_path * constr array | IsAbst of section_path * constr array | IsEvar of int * constr array @@ -146,7 +146,7 @@ val mkNamedLambda : identifier -> constr -> constr -> constr (* If $a = [| t_1; \dots; t_n |]$, constructs the application $(t_1~\dots~t_n)$. *) val mkAppL : constr array -> constr -val mkAppList : constr list -> constr +val mkAppList : constr -> constr list -> constr (* Constructs a constant *) (* The array of terms correspond to the variables introduced in the section *) diff --git a/kernel/typeops.mli b/kernel/typeops.mli index f87601299..cb7f97ec5 100644 --- a/kernel/typeops.mli +++ b/kernel/typeops.mli @@ -10,7 +10,7 @@ open Environ (*i*) -(* Base operations of the typing machine. *) +(* Basic operations of the typing machine. *) val make_judge : constr -> typed_type -> unsafe_judgment diff --git a/kernel/typing.ml b/kernel/typing.ml index 8a18c1e2b..27b50dceb 100644 --- a/kernel/typing.ml +++ b/kernel/typing.ml @@ -94,13 +94,9 @@ let rec execute mf env cstr = | IsSort (Type u) -> type_of_type u - | IsAppL a -> - let la = Array.length a in - if la = 0 then error_cant_execute CCI env cstr; - let hd = a.(0) - and tl = Array.to_list (Array.sub a 1 (la - 1)) in - let (j,cst1) = execute mf env hd in - let (jl,cst2) = execute_list mf env tl in + | 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 cst = Constraint.union cst1 (Constraint.union cst2 cst3) in (j, cst) |