From 0159c363e87c619f41fb030e4a8c2338761fbad2 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 10 Jul 2001 13:59:55 +0000
Subject: Branchement sur bad_tactic_args

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1846 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 tactics/dhyp.ml | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/tactics/dhyp.ml b/tactics/dhyp.ml
index 95f8f170ea..211ecbf6dd 100644
--- a/tactics/dhyp.ml
+++ b/tactics/dhyp.ml
@@ -290,13 +290,13 @@ let _=
   add_tactic "DHyp"
     (function
        | [Identifier id] -> dHyp id
-       | _ -> bad_tactic_args "DHyp")
+       | l -> bad_tactic_args "DHyp" l)
 
 let _=
   add_tactic "CDHyp"
     (function
        | [Identifier id] -> cDHyp id
-       | _ -> bad_tactic_args "CDHyp")
+       | l -> bad_tactic_args "CDHyp" l)
 
 (* [DConcl gls]
 
@@ -313,7 +313,7 @@ let _=
   add_tactic "DConcl"
     (function
        | [] -> dConcl
-       | _ -> bad_tactic_args "DConcl")
+       | l -> bad_tactic_args "DConcl" l)
 
 let to2Lists (table : t) = Nbtermdn.to2lists table
 
@@ -336,6 +336,6 @@ let sarch_depth_tdb = ref(5)
 let dyn_auto_tdb = function 
   | [Integer n] -> auto_tdb n 
   | []          -> auto_tdb !sarch_depth_tdb
-  | _           -> bad_tactic_args "AutoTDB"
+  | l           -> bad_tactic_args "AutoTDB" l
 
 let h_auto_tdb = hide_tactic "AutoTDB" dyn_auto_tdb
-- 
cgit v1.2.3