diff options
| author |  jforest <jforest@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-07-13 10:36:24 +0000 |
|---|---|---|
| committer | jforest <jforest@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-07-13 10:36:24 +0000 |
| commit | ace68194290b49c459a56ea0a023863056fae0e2 (patch) | |
| tree | b61ecae03d65b8157f1760a60e64f107ef341447 /contrib/recdef/recdef.ml4 | |
| parent | b31209570658a78d8c66b5dc640a1fd949d2d305 (diff) | |
removing a warning at compilation time
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9991 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/recdef/recdef.ml4')
| -rw-r--r-- | contrib/recdef/recdef.ml4 | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/contrib/recdef/recdef.ml4 b/contrib/recdef/recdef.ml4 index afbe1c933..31c9659b1 100644 --- a/contrib/recdef/recdef.ml4 +++ b/contrib/recdef/recdef.ml4 @@ -1415,7 +1415,7 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num with e -> begin if Tacinterp.get_debug () <> Tactic_debug.DebugOff - then anomalylabstrm "" (str "Cannot create equation Lemma " ++ Cerrors.explain_exn e) + then pperrnl (str "Cannot create equation Lemma " ++ Cerrors.explain_exn e) else anomaly "Cannot create equation Lemma" ; (* ignore(try Vernacentries.vernac_reset_name (Util.dummy_loc,functional_id) with _ -> ()); *) |