- Add more precise error localisation when one of the application fails

  in a chain of apply or apply-in.
- Improved comments on the notions of permutation used in the library (still
  the equality relation in file Permutation.v misses the property of being
  effectively an equivalence relation, hence missing expected properties of
  this notion of permutation).



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

10 files changed, 52 insertions, 34 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index daf97d529..741753521 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -722,7 +722,7 @@ let unify_resolve_nodelta (c,clenv) gl =
 let unify_resolve flags (c,clenv) gl = 
   let clenv' = connect_clenv gl clenv in
   let _ = clenv_unique_resolver false ~flags clenv' gl in  
-  h_apply true false [inj_open c,NoBindings] gl
+  h_apply true false [dummy_loc,(inj_open c,NoBindings)] gl
 
 let unify_resolve_gen = function
   | None -> unify_resolve_nodelta
diff --git a/tactics/hiddentac.ml b/tactics/hiddentac.ml
index 65a56100b..e6130cfcd 100644
--- a/tactics/hiddentac.ml
+++ b/tactics/hiddentac.ml
@@ -40,10 +40,10 @@ let h_exact_no_check c =
 let h_vm_cast_no_check c = 
   abstract_tactic (TacVmCastNoCheck (inj_open c)) (vm_cast_no_check c)
 let h_apply simple ev cb =
-  abstract_tactic (TacApply (simple,ev,cb,None))
+  abstract_tactic (TacApply (simple,ev,List.map snd cb,None))
     (apply_with_ebindings_gen simple ev cb)
 let h_apply_in simple ev cb (id,ipat as inhyp) =
-  abstract_tactic (TacApply (simple,ev,cb,Some inhyp))
+  abstract_tactic (TacApply (simple,ev,List.map snd cb,Some inhyp))
     (apply_in simple ev id cb ipat)
 let h_elim ev cb cbo    =
   abstract_tactic (TacElim (ev,inj_open_wb cb,Option.map inj_open_wb cbo))
@@ -131,8 +131,8 @@ let h_transitivity c =
   abstract_tactic (TacTransitivity (Option.map inj_open c))
     (intros_transitivity c)
 
-let h_simplest_apply c  = h_apply false false [inj_open c,NoBindings]
-let h_simplest_eapply c = h_apply false true [inj_open c,NoBindings]
+let h_simplest_apply c = h_apply false false [dummy_loc,(inj_open c,NoBindings)]
+let h_simplest_eapply c = h_apply false true [dummy_loc,(inj_open c,NoBindings)]
 let h_simplest_elim c   = h_elim false (c,NoBindings) None
 let h_simplest_case   c = h_case false (c,NoBindings)
 
diff --git a/tactics/hiddentac.mli b/tactics/hiddentac.mli
index f5b2dbb55..6f592108b 100644
--- a/tactics/hiddentac.mli
+++ b/tactics/hiddentac.mli
@@ -38,9 +38,9 @@ val h_exact_no_check  : constr -> tactic
 val h_vm_cast_no_check  : constr -> tactic
 
 val h_apply           : advanced_flag -> evars_flag -> 
-  open_constr with_bindings list -> tactic
+  open_constr with_bindings located list -> tactic
 val h_apply_in        : advanced_flag -> evars_flag -> 
-  open_constr with_bindings list -> 
+  open_constr with_bindings located list -> 
   identifier * intro_pattern_expr located option -> tactic
 
 val h_elim            : evars_flag -> constr with_ebindings ->
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index e436fc90f..32c69ddcd 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1731,6 +1731,17 @@ let interp_constr_with_bindings ist gl (c,bl) =
 let interp_open_constr_with_bindings ist gl (c,bl) =
   (pf_interp_open_constr false ist gl c, interp_bindings ist gl bl)
 
+let loc_of_bindings = function
+| NoBindings -> dummy_loc
+| ImplicitBindings l -> loc_of_rawconstr (fst (list_last l))
+| ExplicitBindings l -> pi1 (list_last l)
+
+let interp_open_constr_with_bindings_loc ist gl ((c,_),bl as cb) =
+  let loc1 = loc_of_rawconstr c in
+  let loc2 = loc_of_bindings bl in
+  let loc = if loc2 = dummy_loc then loc1 else join_loc loc1 loc2 in
+  (loc,interp_open_constr_with_bindings ist gl cb)
+
 let interp_induction_arg ist gl = function
   | ElimOnConstr c -> ElimOnConstr (interp_constr_with_bindings ist gl c)
   | ElimOnAnonHyp n as x -> x
@@ -2230,9 +2241,9 @@ and interp_atomic ist gl = function
   | TacExactNoCheck c -> h_exact_no_check (pf_interp_constr ist gl c)
   | TacVmCastNoCheck c -> h_vm_cast_no_check (pf_interp_constr ist gl c)
   | TacApply (a,ev,cb,None) ->
-      h_apply a ev (List.map (interp_open_constr_with_bindings ist gl) cb)
+      h_apply a ev (List.map (interp_open_constr_with_bindings_loc ist gl) cb)
   | TacApply (a,ev,cb,Some cl) ->
-      h_apply_in a ev (List.map (interp_open_constr_with_bindings ist gl) cb)
+      h_apply_in a ev (List.map (interp_open_constr_with_bindings_loc ist gl) cb)
         (interp_in_hyp_as ist gl cl)
   | TacElim (ev,cb,cbo) ->
       h_elim ev (interp_constr_with_bindings ist gl cb)
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 0224da6c8..ca64a8d3d 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -840,7 +840,7 @@ let check_evars sigma evm gl =
     errorlabstrm "apply" (str"Uninstantiated existential variables: " ++ 
       fnl () ++ pr_evar_defs rest)
 
-let general_apply with_delta with_destruct with_evars (c,lbind) gl0 =
+let general_apply with_delta with_destruct with_evars (loc,(c,lbind)) gl0 =
   let flags = 
     if with_delta then default_unify_flags else default_no_delta_unify_flags in
   (* The actual type of the theorem. It will be matched against the
@@ -874,9 +874,9 @@ let general_apply with_delta with_destruct with_evars (c,lbind) gl0 =
 	    with PretypeError _|RefinerError _|UserError _|Failure _|Exit ->
 	      if with_destruct then
                 descend_in_conjunctions with_evars
-                  try_main_apply (fun _ -> raise exn) c gl
+                  try_main_apply (fun _ -> Stdpp.raise_with_loc loc exn) c gl
 	      else
-		raise exn
+		Stdpp.raise_with_loc loc exn
 	in try_red_apply thm_ty0 
   in
     if evm = Evd.empty then try_main_apply with_destruct c gl0
@@ -888,19 +888,18 @@ let general_apply with_delta with_destruct with_evars (c,lbind) gl0 =
 let rec apply_with_ebindings_gen b e = function
   | [] ->
       tclIDTAC
-  | [cb] ->
-      general_apply b b e cb
+  | [cb] -> general_apply b b e cb
   | cb::cbl -> 
       tclTHENLAST (general_apply b b e cb) (apply_with_ebindings_gen b e cbl)
 
-let apply_with_ebindings cb = apply_with_ebindings_gen false false [cb]
-let eapply_with_ebindings cb = apply_with_ebindings_gen false true [cb]
+let apply_with_ebindings cb = apply_with_ebindings_gen false false [dloc,cb]
+let eapply_with_ebindings cb = apply_with_ebindings_gen false true [dloc,cb]
 
 let apply_with_bindings (c,bl) =
   apply_with_ebindings (inj_open c,inj_ebindings bl)
 
 let eapply_with_bindings (c,bl) =
-  apply_with_ebindings_gen false true [inj_open c,inj_ebindings bl]
+  apply_with_ebindings_gen false true [dloc,(inj_open c,inj_ebindings bl)]
 
 let apply c =
   apply_with_ebindings (inj_open c,NoBindings)
@@ -947,7 +946,8 @@ let apply_in_once_main flags innerclause (d,lbind) gl =
     with NotExtensibleClause -> raise err in 
   aux (make_clenv_binding gl (d,thm) lbind)
 
-let apply_in_once with_delta with_destruct with_evars id ((sigma,d),lbind) gl0 =
+let apply_in_once with_delta with_destruct with_evars id 
+  (loc,((sigma,d),lbind)) gl0 =
   let flags = 
     if with_delta then default_unify_flags else default_no_delta_unify_flags in
   let t' = pf_get_hyp_typ gl0 id in
@@ -1141,7 +1141,8 @@ let constructor_tac with_evars expctdnumopt i lbind gl =
     Array.length (snd (Global.lookup_inductive mind)).mind_consnames in
   check_number_of_constructors expctdnumopt i nconstr;
   let cons = mkConstruct (ith_constructor_of_inductive mind i) in
-  let apply_tac = general_apply true false with_evars (inj_open cons,lbind) in
+  let apply_tac =
+    general_apply true false with_evars (dloc,(inj_open cons,lbind)) in
   (tclTHENLIST 
      [convert_concl_no_check redcl DEFAULTcast; intros; apply_tac]) gl
 
@@ -1374,6 +1375,9 @@ let general_apply_in with_delta with_destruct with_evars id lemmas ipat gl =
 
 let apply_in simple with_evars = general_apply_in simple simple with_evars
 
+let simple_apply_in id c = 
+  apply_in false false id [dloc,((Evd.empty,c),NoBindings)] None
+
 (**************************)
 (*   Generalize tactics   *)
 (**************************)
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 40740c3a8..6e52546f4 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -180,7 +180,8 @@ val apply                 : constr -> tactic
 val eapply                : constr -> tactic
 
 val apply_with_ebindings_gen : 
-  advanced_flag -> evars_flag -> open_constr with_ebindings list -> tactic
+  advanced_flag -> evars_flag -> open_constr with_ebindings located list ->
+    tactic
 
 val apply_with_bindings   : constr with_bindings -> tactic
 val eapply_with_bindings  : constr with_bindings -> tactic
@@ -192,9 +193,11 @@ val cut_and_apply         : constr -> tactic
 
 val apply_in : 
   advanced_flag -> evars_flag -> identifier -> 
-  open_constr with_ebindings list ->
+  open_constr with_ebindings located list ->
   intro_pattern_expr located option -> tactic
 
+val simple_apply_in : identifier -> constr -> tactic
+
 (*s Elimination tactics. *)
 
 
diff --git a/theories/Lists/List.v b/theories/Lists/List.v
index 7e9711bba..6582b2a87 100644
--- a/theories/Lists/List.v
+++ b/theories/Lists/List.v
@@ -785,11 +785,10 @@ Section ListOps.
   End Reverse_Induction.
 
 
+  (*********************************************************************)
+  (** ** List permutations as a composition of adjacent transpositions *)
+  (*********************************************************************)
 
-  (***********************************)
-  (** ** Lists modulo permutation    *)
-  (***********************************)
-  
   Section Permutation.
 
     Inductive Permutation : list A -> list A -> Prop :=
diff --git a/theories/Sorting/PermutSetoid.v b/theories/Sorting/PermutSetoid.v
index 814ef0408..1ea71972b 100644
--- a/theories/Sorting/PermutSetoid.v
+++ b/theories/Sorting/PermutSetoid.v
@@ -13,7 +13,7 @@ Require Import Omega Relations Multiset Permutation SetoidList.
 Set Implicit Arguments.
 
 (** This file contains additional results about permutations 
-     with respect to an setoid equality (i.e. an equivalence relation). 
+     with respect to a setoid equality (i.e. an equivalence relation). 
 *)
 
 Section Perm.
diff --git a/theories/Sorting/Permutation.v b/theories/Sorting/Permutation.v
index e9bbf88e3..a92212054 100644
--- a/theories/Sorting/Permutation.v
+++ b/theories/Sorting/Permutation.v
@@ -12,22 +12,23 @@ Require Import Relations List Multiset Arith.
 
 (** This file define a notion of permutation for lists, based on multisets: 
     there exists a permutation between two lists iff every elements have 
-    the same multiplicities in the two lists. 
+    the same multiplicity in the two lists. 
+
+    Unlike [List.Permutation], the present notion of permutation
+    requires the domain to be equipped with a decidable equality. This
+    equality allows to reason modulo the effective equivalence-class
+    representative used in each list.
 
-    Unlike [List.Permutation], the present notion of permutation requires
-    a decidable equality. At the same time, this definition can be used 
-    with a non-standard equality, whereas [List.Permutation] cannot.
-      
     The present file contains basic results, obtained without any particular
     assumption on the decidable equality used.
-	
+
     File [PermutSetoid] contains additional results about permutations 
     with respect to an setoid equality (i.e. an equivalence relation). 
 
     Finally, file [PermutEq] concerns Coq equality : this file is similar 
     to the previous one, but proves in addition that [List.Permutation]
     and [permutation] are equivalent in this context.
-x*)
+*)
 
 Set Implicit Arguments.
 
diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml
index 66d02278c..5ddf2b705 100644
--- a/toplevel/auto_ind_decl.ml
+++ b/toplevel/auto_ind_decl.ml
@@ -535,7 +535,7 @@ repeat ( apply andb_prop in z;let z1:= fresh "Z" in destruct z as [z1 z]).
 *)
                     tclREPEAT (
                       tclTHENSEQ [
-                         apply_in false false freshz [(Evd.empty,andb_prop()),Rawterm.NoBindings] None;
+                         simple_apply_in freshz (andb_prop());
                          fun gl ->
                            let fresht = fresh_id (!avoid) (id_of_string "Z") gsig 
                            in