- Temptative change to notations like "as [|n H]_eqn" or "as [|n H]_eqn:H",

  and, with a now generic intropattern "[]", also "as []_eqn", "as []_eqn:H"
  for "destruct" with equality keeping.
- Fixed an accuracy loss in error location.


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

7 files changed, 37 insertions, 15 deletions

diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index 1f4aa8b24f..a531770a46 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -257,6 +257,11 @@ GEXTEND Gram
       | "?" -> loc, IntroAnonymous
       | id = ident -> loc, IntroIdentifier id ] ]
   ;
+  intropattern_modifier:
+    [ [ IDENT "_eqn"; 
+        id = [ ":"; id = naming_intropattern -> id | -> loc, IntroAnonymous ]
+        -> id ] ]
+  ;
   simple_intropattern:
     [ [ pat = disjunctive_intropattern -> pat
       | pat = naming_intropattern -> pat
@@ -415,13 +420,12 @@ GEXTEND Gram
       | -> None ] ]
   ;
   with_inversion_names:
-    [ [ "as"; ipat = disjunctive_intropattern -> Some ipat
+    [ [ "as"; ipat = simple_intropattern -> Some ipat
       | -> None ] ]
   ;
   with_induction_names:
-    [ [ "as"; eq = OPT naming_intropattern; ipat = disjunctive_intropattern
+    [ [ "as"; ipat = simple_intropattern; eq = OPT intropattern_modifier
         -> (eq,Some ipat)
-      | "as"; eq = naming_intropattern -> (Some eq,None)
       | -> (None,None) ] ]
   ;
   as_name:
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 568b6ea42a..7413909b53 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -96,7 +96,7 @@ let catch_error call_trace tac g =
     let (loc',c),tail = list_sep_last call_trace in
     let loc,e' = match e with Stdpp.Exc_located(loc,e) -> loc,e | _ ->dloc,e in
     if tail = [] then
-      let loc = if loc' = dloc then loc else loc' in
+      let loc = if loc = dloc then loc' else loc in
       raise (Stdpp.Exc_located(loc,e'))
     else
       raise (Stdpp.Exc_located(loc',LtacLocated((c,tail,loc),e')))
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 9ea8a459c7..6bded84dd1 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -283,6 +283,13 @@ type branch_assumptions = {
   ba        : branch_args;     (* the branch args *)
   assums    : named_context}   (* the list of assumptions introduced *)
 
+let fix_empty_or_and_pattern nv l =
+  (* 1- The syntax does not distinguish between "[ ]" for one clause with no 
+     names and "[ ]" for no clause at all *)
+  (* 2- More generally, we admit "[ ]" for any disjunctive pattern of 
+     arbitrary length *)
+  if l = [[]] then list_make nv [] else l
+
 let check_or_and_pattern_size loc names n =
   if List.length names <> n then
     if n = 1 then 
@@ -295,10 +302,11 @@ let compute_induction_names n = function
   | None ->
       Array.make n []
   | Some (loc,IntroOrAndPattern names) ->
+      let names = fix_empty_or_and_pattern n names in
       check_or_and_pattern_size loc names n;
       Array.of_list names
-  | _ ->
-      error "Unexpected introduction pattern."
+  | Some (loc,_) ->
+      user_err_loc (loc,"",str "Disjunctive/conjunctive introduction pattern expected.")
 
 let compute_construtor_signatures isrec (_,k as ity) =
   let rec analrec c recargs =
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli
index 6cd63fa6ad..7f2c366f7d 100644
--- a/tactics/tacticals.mli
+++ b/tactics/tacticals.mli
@@ -139,6 +139,10 @@ type branch_assumptions = {
 val check_or_and_pattern_size :
   Util.loc -> or_and_intro_pattern_expr -> int -> unit 
 
+(* Tolerate "[]" to mean a disjunctive pattern of any length *)
+val fix_empty_or_and_pattern : int -> or_and_intro_pattern_expr -> 
+  or_and_intro_pattern_expr
+
 (* Useful for [as intro_pattern] modifier *)
 val compute_induction_names : 
   int -> intro_pattern_expr located option -> 
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index c8d078aee2..79498076b2 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1094,11 +1094,6 @@ let register_general_multi_rewrite f =
 let clear_last = tclLAST_HYP (fun c -> (clear [destVar c]))
 let case_last  = tclLAST_HYP simplest_case
 
-let fix_empty_case nv l =
-  (* The syntax does not distinguish between "[ ]" for one clause with no names
-     and "[ ]" for no clause at all; so we are a bit liberal here *)
-  if Array.length nv = 0 & l = [[]] then [] else l
-
 let error_unexpected_extra_pattern loc nb pat =
   let s1,s2,s3 = match pat with
   | IntroIdentifier _ -> "name", (plural nb " introduction pattern"), "no"
@@ -1121,7 +1116,7 @@ let intro_or_and_pattern loc b ll l' tac =
 	  if bracketed then error_unexpected_extra_pattern loc' nb pat;
 	  l
       | ip :: l -> ip :: adjust_names_length nb (n-1) l in
-    let ll = fix_empty_case nv ll in
+    let ll = fix_empty_or_and_pattern (Array.length nv) ll in
     check_or_and_pattern_size loc ll (Array.length nv);
     tclTHENLASTn
       (tclTHEN case_last clear_last)
diff --git a/theories/Init/Tactics.v b/theories/Init/Tactics.v
index 2e0fe42b68..a59eba6f46 100644
--- a/theories/Init/Tactics.v
+++ b/theories/Init/Tactics.v
@@ -72,6 +72,17 @@ Ltac false_hyp H G :=
 
 Ltac case_eq x := generalize (refl_equal x); pattern x at -1; case x.
 
+(* Similar variants of destruct *)
+
+Tactic Notation "destruct_with_eqn" constr(x) :=
+  destruct x as []_eqn.
+Tactic Notation "destruct_with_eqn" ident(n) := 
+  try intros until n; destruct n as []_eqn.
+Tactic Notation "destruct_with_eqn" ":" ident(H) constr(x) :=
+  destruct x as []_eqn:H.
+Tactic Notation "destruct_with_eqn" ":" ident(H) ident(n) := 
+  try intros until n; destruct n as []_eqn:H.
+
 (* Rewriting in all hypothesis several times everywhere *)
 
 Tactic Notation "rewrite_all" constr(eq) := repeat rewrite eq in *.
diff --git a/theories/NArith/Ndigits.v b/theories/NArith/Ndigits.v
index a3326ccd3c..ea5f02bba9 100644
--- a/theories/NArith/Ndigits.v
+++ b/theories/NArith/Ndigits.v
@@ -511,7 +511,7 @@ Lemma Nless_trans :
    Nless a a' = true -> Nless a' a'' = true -> Nless a a'' = true.
 Proof.
   induction a as [|a IHa|a IHa] using N_ind_double; intros a' a'' H H0.
-    destruct (Nless N0 a'') as Heqb in *. trivial.
+    destruct (Nless N0 a'') as []_eqn:Heqb. trivial.
      rewrite (N0_less_2 a'' Heqb), (Nless_z a') in H0. discriminate H0.
     induction a' as [|a' _|a' _] using N_ind_double.
       rewrite (Nless_z (Ndouble a)) in H. discriminate H.
@@ -539,10 +539,10 @@ Lemma Nless_total :
  forall a a', {Nless a a' = true} + {Nless a' a = true} + {a = a'}.
 Proof.
   induction a using N_rec_double; intro a'.
-    destruct (Nless N0 a') as Heqb in *. left. left. auto.
+    destruct (Nless N0 a') as []_eqn:Heqb. left. left. auto.
      right. rewrite (N0_less_2 a' Heqb). reflexivity.
     induction a' as [|a' _|a' _] using N_rec_double.
-      destruct (Nless N0 (Ndouble a)) as Heqb in *. left. right. auto.
+      destruct (Nless N0 (Ndouble a)) as []_eqn:Heqb. left. right. auto.
        right. exact (N0_less_2 _  Heqb).
       rewrite 2!Nless_def_1. destruct (IHa a') as [ | ->].
         left. assumption.