gros commit de tout ce que j'ai fait pendant les vacances :

 - tactics/Equality
 - debug du discharge
 - constr_of_compattern implante vite fait / mal fait en attendant mieux
 - theories/Logic (ne passe pas entierrement)


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

7 files changed, 27 insertions, 4 deletions

diff --git a/kernel/environ.ml b/kernel/environ.ml
index c8c85c76e..7507be838 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -193,6 +193,8 @@ let named_hd env a = function
 
 let prod_name env (n,a,b) = mkProd (named_hd env a n) a b
 
+let lambda_create env (a,b) =  mkLambda (named_hd env a Anonymous) a b
+
 (* Abstractions. *)
 
 let evaluable_abst env = function
diff --git a/kernel/environ.mli b/kernel/environ.mli
index 6d38ad819..31edb0d7f 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -53,6 +53,7 @@ val id_of_global : env -> sorts oper -> identifier
 val id_of_name_using_hdchar : env -> constr -> name -> identifier
 val named_hd : env -> constr -> name -> name
 val prod_name : env -> name * constr * constr -> constr
+val lambda_create : env -> constr * constr -> constr
 
 val translucent_abst : env -> constr -> bool
 val evaluable_abst : env -> constr -> bool
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index d7f8b8386..b2c5df74f 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -434,6 +434,19 @@ let add_mind sp mie env =
 
 let add_constraints = add_constraints
 
+let pop_vars idl env =
+  let rec remove n sign = 
+    if n = 0 then
+      sign
+    else
+      match sign with
+	| (id::ids,_::tys) ->
+	    if not (List.mem id idl) then anomaly "pop_vars";
+	    remove (pred n) (ids,tys) 
+	| _ -> anomaly "pop_vars"
+  in
+  change_hyps (remove (List.length idl)) env
+
 let export = export
 let import = import
 
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index afa8d3ef9..07e95197c 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -40,6 +40,8 @@ val add_mind :
     -> safe_environment
 val add_constraints : constraints -> safe_environment -> safe_environment
 
+val pop_vars : identifier list -> safe_environment -> safe_environment
+
 val lookup_var : identifier -> safe_environment -> name * typed_type
 val lookup_rel : int -> safe_environment -> name * typed_type
 val lookup_constant : section_path -> safe_environment -> constant_body
diff --git a/kernel/term.ml b/kernel/term.ml
index 56dd87f8f..411326106 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -424,6 +424,10 @@ let destEvar = function
   | DOPN (Evar n, a) -> (n,a)
   | _ -> invalid_arg "destEvar"
 
+let num_of_evar = function
+  | DOPN (Evar n, _) -> n
+  | _ -> anomaly "num_of_evar called with bad args"
+
 (* Destructs an abstract term *)
 let destAbst = function
   | DOPN (Abst sp, a) -> (sp, a)
diff --git a/kernel/term.mli b/kernel/term.mli
index a7f2e6180..ab1db881a 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -288,6 +288,7 @@ val args_of_const : constr -> constr array
 
 (* Destructs an existential variable *)
 val destEvar : constr -> int * constr array
+val num_of_evar : constr -> int
 
 (* Destrucy an abstract term *)
 val destAbst : constr -> section_path * constr array
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 1254d5ef9..4b20f3b0a 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -84,7 +84,7 @@ let check_hyps id env sigma hyps =
 let type_of_constant env sigma (sp,args) =
   let cb = lookup_constant sp env in
   let hyps = cb.const_hyps in
-  check_hyps (basename sp) env sigma hyps;
+  (* TODO: check args *)
   instantiate_type (ids_of_sign hyps) cb.const_type (Array.to_list args)
 
 (* Inductive types. *)
@@ -99,7 +99,7 @@ let instantiate_arity mis =
 let type_of_inductive env sigma i =
   let mis = lookup_mind_specif i env in
   let hyps = mis.mis_mib.mind_hyps in
-  check_hyps (basename mis.mis_sp) env sigma hyps;
+  (* TODO: check args *)
   instantiate_arity mis
 
 (* Constructors. *)
@@ -112,7 +112,7 @@ let instantiate_lc mis =
 let type_of_constructor env sigma ((ind_sp,j),args as cstr) =
   let mind = inductive_of_constructor cstr in
   let mis = lookup_mind_specif mind env in
-  check_hyps (basename mis.mis_sp) env sigma (mis.mis_mib.mind_hyps);
+  (* TODO: check args *)
   let specif = instantiate_lc mis in
   let make_ik k = DOPN (MutInd (mis.mis_sp,k), mis.mis_args) in
   if j > mis_nconstr mis then
@@ -161,7 +161,7 @@ let type_of_existential env sigma c =
   let evi = Evd.map sigma ev in
   let hyps = var_context evi.Evd.evar_env in
   let id = id_of_string ("?" ^ string_of_int ev) in
-  check_hyps id env sigma hyps;
+  (* TODO: check args *)
   instantiate_constr (ids_of_sign hyps) evi.Evd.evar_concl (Array.to_list args)