Branchement sur bad_tactic_args

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

2 files changed, 16 insertions, 15 deletions

diff --git a/tactics/inv.ml b/tactics/inv.ml
index 65e49d1186..1c4990143a 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -429,7 +429,7 @@ let (half_inv_tac, inv_tac, inv_clear_tac) =
     hide_tactic "Inv"
       (function
 	 | [ic; Identifier id] -> inv false (com_of_id ic) NoDep id
-	 | _ -> anomaly "Inv called with bad args")
+	 | l -> bad_tactic_args "Inv" l)
   in
   ((fun id -> gentac [hinv_kind; Identifier id]),
    (fun id -> gentac [inv_kind; Identifier id]),
@@ -441,7 +441,7 @@ let named_inv =
     hide_tactic "NamedInv"
       (function
 	 | [ic; Identifier id] -> inv true (com_of_id ic) NoDep id
-	 | _ -> anomaly "NamedInv called with bad args")
+	 | l -> bad_tactic_args "NamedInv" l)
   in 
   (fun ic id -> gentac [ic; Identifier id])
 
@@ -451,7 +451,7 @@ let (half_dinv_tac, dinv_tac, dinv_clear_tac) =
     hide_tactic "DInv"
       (function
 	 | [ic; Identifier id] -> inv false (com_of_id ic) (Dep None) id
-	 | _ -> anomaly "DInv called with bad args")
+	 | l -> bad_tactic_args "DInv" l)
   in
   ((fun id -> gentac [hinv_kind; Identifier id]),
    (fun id -> gentac [inv_kind; Identifier id]),
@@ -468,7 +468,7 @@ let (half_dinv_with, dinv_with, dinv_clear_with) =
 		 (Dep (Some (pf_interp_constr gls com))) id gls
 	 | [ic; Identifier id; Constr c] ->
              fun gls -> inv false (com_of_id ic) (Dep (Some c)) id gls
-	 | _ -> anomaly "DInvWith called with bad args")
+	 | l -> bad_tactic_args "DInvWith" l)
   in
   ((fun id c -> gentac [hinv_kind; Identifier id; Constr c]),
    (fun id c -> gentac [inv_kind; Identifier id; Constr c]),
@@ -500,14 +500,15 @@ let invIn_tac =
   let gentac =
     hide_tactic "InvIn"
       (function
-	 | (com::(Identifier id)::hl) ->
+	 | (com::(Identifier id)::hl as ll) ->
 	     let hl' =
-	       List.map (function
-			   | Identifier id -> id
-			   | _ -> anomaly "InvIn called with bas args") hl 
+	       List.map
+		 (function
+		    | Identifier id -> id
+		    | _ -> bad_tactic_args "InvIn" ll) hl 
 	     in
              invIn (com_of_id com) id hl'
-	 | _ -> anomaly "InvIn called with bad args")
+	 | ll -> bad_tactic_args "InvIn" ll)
   in 
   fun com id hl ->
     gentac
diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index 39b2c7a738..e168287afd 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -356,7 +356,7 @@ let useInversionLemma =
              fun gls -> lemInv id (pf_interp_constr gls com) gls
 	 | [Identifier id; Constr c] ->
              fun gls -> lemInv id c gls
-	 | _  -> anomaly "useInversionLemma")
+	 | l  -> bad_vernac_args "useInversionLemma" l)
   in 
   fun id c -> gentac [Identifier id;Constr c]
 
@@ -380,21 +380,21 @@ let useInversionLemmaIn =
   let gentac =
     hide_tactic "UseInversionLemmaIn"
       (function
-	 | ((Identifier id)::(Command com)::hl) ->
+	 | ((Identifier id)::(Command com)::hl as ll) ->
 	     fun gls ->
 	       lemInvIn id (pf_interp_constr gls com)
                  (List.map
 		    (function
 		       | (Identifier id) -> id
-		       | _ -> anomaly "UseInversionLemmaIn") hl) gls
-	 | ((Identifier id)::(Constr c)::hl) ->
+		       | _ -> bad_vernac_args "UseInversionLemmaIn" ll) hl) gls
+	 | ((Identifier id)::(Constr c)::hl as ll) ->
 	     fun gls ->
 	       lemInvIn id c
                  (List.map
 		    (function
 		       | (Identifier id) -> id
-		       | _ -> anomaly "UseInversionLemmaIn") hl) gls
-	 | _ -> anomaly "UseInversionLemmaIn")
+		       | _ -> bad_vernac_args "UseInversionLemmaIn" ll) hl) gls
+	 | ll -> bad_vernac_args "UseInversionLemmaIn" ll)
   in 
   fun id c hl ->
     gentac ((Identifier id)::(Constr c)