From f2da732ffd5db2b93a2c8120c668f8b2f6068d3b Mon Sep 17 00:00:00 2001
From: filliatr
Date: Tue, 7 Dec 1999 14:56:36 +0000
Subject: debuggage inductifs (suite) / compilation Dhyp et Auto (mais pas
 linkes

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@220 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 proofs/tacinterp.ml  | 4 ++++
 proofs/tacinterp.mli | 2 ++
 2 files changed, 6 insertions(+)

(limited to 'proofs')

diff --git a/proofs/tacinterp.ml b/proofs/tacinterp.ml
index 3413b2a614..9e6f3006ea 100644
--- a/proofs/tacinterp.ml
+++ b/proofs/tacinterp.ml
@@ -154,3 +154,7 @@ let vernac_interp_atomic =
 	 | _ -> assert false)
   in 
   fun opn args -> gentac ((Identifier opn)::args)
+
+let bad_tactic_args s =
+  anomalylabstrm s
+    [< 'sTR"Tactic "; 'sTR s; 'sTR" called with bad arguments" >]
diff --git a/proofs/tacinterp.mli b/proofs/tacinterp.mli
index aa71f411dc..3e913f808a 100644
--- a/proofs/tacinterp.mli
+++ b/proofs/tacinterp.mli
@@ -24,3 +24,5 @@ val vernac_interp_atomic : identifier -> tactic_arg list -> tactic
 val overwriting_tacinterp_add : string * (tactic_arg list -> tactic) -> unit
 val is_just_undef_macro     : Coqast.t -> string option
 
+val bad_tactic_args : string -> 'a
+
-- 
cgit v1.2.3