- documentation repertoire proofs/

 - IsAppL of constr * constr list ==> répercussion
 - module Clenv (suite; as terminé)


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@113 85f007b7-540e-0410-9357-904b9bb8a0f7

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)