diff options
| author | herbelin | 2001-07-10 13:59:55 +0000 |
|---|---|---|
| committer | herbelin | 2001-07-10 13:59:55 +0000 |
| commit | 0159c363e87c619f41fb030e4a8c2338761fbad2 (patch) | |
| tree | 40842adbc171df76ac2e541d2879b66fcdf2191a | |
| parent | df6bdefc9a7cd63b8409632e3f2cbc090ed1f236 (diff) | |
Branchement sur bad_tactic_args
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1846 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | tactics/dhyp.ml | 8 |
1 files 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 |