From aec4317b506e4f47b292cfc5ca79a3b025cf854d Mon Sep 17 00:00:00 2001
From: barras
Date: Mon, 7 May 2001 12:18:43 +0000
Subject: quelques bug reports mineurs

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

(limited to 'proofs')

diff --git a/proofs/tacinterp.ml b/proofs/tacinterp.ml
index c6c8cfe6cd..6730419a99 100644
--- a/proofs/tacinterp.ml
+++ b/proofs/tacinterp.ml
@@ -579,8 +579,8 @@ and app_interp (evc,env,lfun,lmatch,goalopt,debug) fv largs ast =
       else
         VFun(olfun@newlfun,lvar,body)
     | _ ->
-      anomaly_loc (Ast.loc ast, "Tacinterp.app_interp",[<'sTR
-        "Illegal application: "; print_ast ast>])
+      user_err_loc (Ast.loc ast, "Tacinterp.app_interp",[<'sTR
+        "Illegal tactic application: "; print_ast ast>])
 
 (* Interprets recursive expressions *)
 and rec_interp (evc,env,lfun,lmatch,goalopt,debug) ast = function
-- 
cgit v1.2.3