- 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

4 files changed, 16 insertions, 9 deletions

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)