diff options
| author | barras | 2001-05-07 12:18:43 +0000 |
|---|---|---|
| committer | barras | 2001-05-07 12:18:43 +0000 |
| commit | aec4317b506e4f47b292cfc5ca79a3b025cf854d (patch) | |
| tree | 80c5b753ddc1b1d116374c3731cb18f277223d75 /proofs | |
| parent | 55426f6fab4f89078134e08f680e52c078b1f5f7 (diff) | |
quelques bug reports mineurs
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1733 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/tacinterp.ml | 4 |
1 files changed, 2 insertions, 2 deletions
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 |