suite du commit precedent

- amelioration des messages d'erreurs de la condition de garde
- reorganisation de clenv.ml


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

3 files changed, 1 insertions, 80 deletions

diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index 6edf56017..fcc1884ca 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -290,7 +290,7 @@ let lemInv id c gls =
   try
     let (wc,kONT) = startWalk gls in
     let clause = mk_clenv_type_of wc c in
-    let clause = clenv_constrain_with_bindings [(Abs (-1),mkVar id)] clause in
+    let clause = clenv_constrain_with_bindings [(-1,mkVar id)] clause in
     res_pf kONT clause gls
   with 
 (* Ce n'est pas l'endroit pour cela
diff --git a/tactics/wcclausenv.ml b/tactics/wcclausenv.ml
index 78f3890c5..f5723fe36 100644
--- a/tactics/wcclausenv.ml
+++ b/tactics/wcclausenv.ml
@@ -29,8 +29,6 @@ open Evar_refiner
    write to Eduardo.Gimenez@inria.fr and ask for the prize :-)
    -- Eduardo (11/8/97) *)
 
-type wc = named_context sigma
-
 let pf_get_new_id id gls = 
   next_ident_away id (pf_ids_of_hyps gls)
 
@@ -40,73 +38,10 @@ let pf_get_new_ids ids gls =
     (fun id acc -> (next_ident_away id (acc@avoid))::acc)
     ids []
 
-type arg_binder =
-  | Dep of identifier
-  | Nodep of int
-  | Abs of int
-
-type arg_bindings = (arg_binder * constr) list
-
-let clenv_constrain_with_bindings bl clause =
-  if bl = [] then 
-    clause 
-  else 
-    let all_mvs = collect_metas (clenv_template clause).rebus
-    and ind_mvs = clenv_independent clause in
-    let nb_indep = List.length ind_mvs in
-    let rec matchrec clause = function
-      | []       -> clause
-      | (b,c)::t ->
-          let k = 
-            match b with
-              | Dep s ->
-		  if List.mem_assoc b t then 
-		    errorlabstrm "clenv_match_args" 
-                      (str "The variable " ++ pr_id s ++ 
-			 str " occurs more than once in binding");
-		  clenv_lookup_name clause s
-              | Nodep n ->
-		  let index = if n > 0 then n-1 else nb_indep+n in
-                  if List.mem_assoc (Nodep (index+1)) t or 
-                    List.mem_assoc (Nodep (index-nb_indep)) t
-                  then errorlabstrm "clenv_match_args"
-                    (str "The position " ++ int n ++
-		       str " occurs more than once in binding");
-		  (try 
-		     List.nth ind_mvs index
-		   with Failure _ ->
-                     errorlabstrm "clenv_constrain_with_bindings"
-                       (str"Clause did not have " ++ int n ++ str"-th" ++
-                          str" unnamed argument"))
-              | Abs n -> 
-                  (try
-                     if n > 0 then 
-		       List.nth all_mvs (n-1)
-                     else if n < 0 then 
-		       List.nth (List.rev all_mvs) (-n-1)
-                     else error "clenv_constrain_with_bindings" 
-                   with Failure _ ->
-                     errorlabstrm "clenv_constrain_with_bindings"
-                       (str"Clause did not have " ++ int n ++ str"-th" ++
-                          str" absolute argument"))
-	  in
-	  let env = Global.env () in
-	  let sigma = Evd.empty in
-	  let k_typ = nf_betaiota (clenv_instance_type clause k) in
-	  let c_typ = nf_betaiota (w_type_of clause.hook c) in 
-	  matchrec
-            (clenv_assign k c (clenv_unify true CUMUL c_typ k_typ clause)) t
-    in 
-    matchrec clause bl
-
 (* What follows is part of the contents of the former file tactics3.ml *)
 (* 2/2002: replaced THEN_i by THENSLAST to solve a bug in
    Tacticals.general_elim when the eliminator has missing bindings *)
 
-let elim_res_pf_THEN_i kONT clenv tac gls =  
-  let clenv' = (clenv_unique_resolver true clenv gls) in
-  tclTHENLASTn (clenv_refine kONT clenv') (tac clenv') gls
-
 let rec build_args acc ce p_0 p_1 =
   match kind_of_term p_0, p_1 with 
     | (Prod (na,a,b), (a_0::bargs)) ->
diff --git a/tactics/wcclausenv.mli b/tactics/wcclausenv.mli
index 45b955326..7493e813c 100644
--- a/tactics/wcclausenv.mli
+++ b/tactics/wcclausenv.mli
@@ -25,17 +25,6 @@ open Clenv
 val pf_get_new_id  : identifier      -> goal sigma -> identifier
 val pf_get_new_ids : identifier list -> goal sigma -> identifier list
 
-type arg_binder = 
-  | Dep of identifier 
-  | Nodep of int 
-  | Abs of int
-
-type arg_bindings = (arg_binder * constr) list
-
-type wc = named_context sigma
-
-val clenv_constrain_with_bindings : arg_bindings -> wc clausenv -> wc clausenv
-
 (*i**
 val add_prod_sign : 
   'a evar_map -> constr * types signature -> constr * types signature
@@ -44,7 +33,4 @@ val add_prods_sign :
   'a evar_map -> constr * types signature -> constr * types signature
 **i*)
 
-val elim_res_pf_THEN_i : 
-  (wc -> tactic) -> wc clausenv -> (wc clausenv -> tactic array) -> tactic
-
 val applyUsing : constr -> tactic