Légère amélioration des messages d'erreur des with-bindings et des Rewrite

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

4 files changed, 13 insertions, 12 deletions

diff --git a/tactics/equality.ml b/tactics/equality.ml
index 4fc8c04e16..494cb50456 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -71,7 +71,7 @@ let general_rewrite_bindings lft2rgt (c,l) gl =
           else
 	    pf_global gl (id_of_string (hdcncls^suffix))
         in 
-	tclNOTSAMEGOAL (general_elim (c,l) (elim,NoBindings)) gl
+	tclNOTSAMEGOAL (general_elim (c,l) (elim,NoBindings) ~allow_K:false) gl
    (* was tclWEAK_PROGRESS which only fails for tactics generating one subgoal 
       and did not fail for useless conditional rewritings generating an
       extra condition *)
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 05b26cbb64..64bf9371fd 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -353,8 +353,8 @@ let glob_constr ist c =
   in c
 
 (* Globalize bindings *)
-let glob_binding ist (b,c) =
-  (glob_quantified_hypothesis ist b,glob_constr ist c)
+let glob_binding ist (loc,b,c) =
+  (loc,glob_quantified_hypothesis ist b,glob_constr ist c)
 
 let glob_bindings ist = function
   | NoBindings -> NoBindings
@@ -1065,8 +1065,8 @@ let interp_induction_arg ist = function
 (*	    (constr_interp ist (Termast.ast_of_qualid (make_short_qualid id)))*)
 	    (constr_interp ist (CRef (Ident (loc,id))))
 
-let binding_interp ist (b,c) =
-  (interp_quantified_hypothesis ist b,constr_interp ist c)
+let binding_interp ist (loc,b,c) =
+  (loc,interp_quantified_hypothesis ist b,constr_interp ist c)
 
 let bindings_interp ist = function
   | NoBindings -> NoBindings
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index e72a35ab4a..eb1829bf6a 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -859,7 +859,7 @@ let last_arg c = match kind_of_term c with
   | App (f,cl) ->  array_last cl
   | _ -> anomaly "last_arg"
 	
-let elimination_clause_scheme kONT elimclause indclause gl = 
+let elimination_clause_scheme kONT elimclause indclause allow_K gl = 
   let indmv = 
     (match kind_of_term (last_arg (clenv_template elimclause).rebus) with
        | Meta mv -> mv
@@ -867,7 +867,7 @@ let elimination_clause_scheme kONT elimclause indclause gl =
              (str "The type of elimination clause is not well-formed")) 
   in
   let elimclause' = clenv_fchain indmv elimclause indclause in 
-  elim_res_pf kONT elimclause' gl
+  elim_res_pf kONT elimclause' allow_K gl
 
 (* cast added otherwise tactics Case (n1,n2) generates (?f x y) and 
  * refine fails *)
@@ -883,14 +883,14 @@ let type_clenv_binding wc (c,t) lbind =
  * matching I, lbindc are the expected terms for c arguments 
  *)
 
-let general_elim (c,lbindc) (elimc,lbindelimc) gl = 
+let general_elim (c,lbindc) (elimc,lbindelimc) ?(allow_K=true) gl = 
   let (wc,kONT)  = startWalk gl in
   let ct = pf_type_of gl c in
   let t = try snd (pf_reduce_to_quantified_ind gl ct) with UserError _ -> ct in
   let indclause  = make_clenv_binding wc (c,t) lbindc  in
   let elimt      = w_type_of wc elimc in
   let elimclause = make_clenv_binding wc (elimc,elimt) lbindelimc in 
-  elimination_clause_scheme kONT elimclause indclause gl
+  elimination_clause_scheme kONT elimclause indclause allow_K gl
 
 (* Elimination tactic with bindings but using the default elimination 
  * constant associated with the type. *)
@@ -1251,7 +1251,7 @@ let induction_tac varname typ (elimc,elimt,lbindelimc) gl =
   let indclause  = make_clenv_binding wc (c,typ) NoBindings  in
   let elimclause =
     make_clenv_binding wc (mkCast (elimc,elimt),elimt) lbindelimc in
-  elimination_clause_scheme kONT elimclause indclause gl
+  elimination_clause_scheme kONT elimclause indclause true gl
 
 let compute_induction_names n names =
   let names = if names = [] then Array.make n [] else Array.of_list names in
@@ -1437,7 +1437,7 @@ let elim_scheme_type elim t gl =
         let clause' =
 	  (* t is inductive, then CUMUL or CONV is irrelevant *)
 	  clenv_unify true CUMUL t (clenv_instance_type clause mv) clause in
-	elim_res_pf kONT clause' gl
+	elim_res_pf kONT clause' true gl
     | _ -> anomaly "elim_scheme_type"
 
 let elim_type t gl =
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 29107c32a2..0c9744e2c6 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -158,7 +158,8 @@ val cut_and_apply         : constr -> tactic
 
 (*s Elimination tactics. *)
 
-val general_elim  : constr with_bindings -> constr with_bindings -> tactic
+val general_elim  : constr with_bindings -> constr with_bindings -> 
+  ?allow_K:bool -> tactic
 val default_elim  : constr with_bindings -> tactic
 val simplest_elim : constr -> tactic
 val elim          : constr with_bindings -> constr with_bindings option -> tactic