From 5a39e6c08d428d774165e0ef3922ba8b75eee9e1 Mon Sep 17 00:00:00 2001 From: ppedrot Date: Mon, 28 Jan 2013 21:05:35 +0000 Subject: Uniformization of the "anomaly" command. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16165 85f007b7-540e-0410-9357-904b9bb8a0f7 --- tactics/eqschemes.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'tactics/eqschemes.ml') diff --git a/tactics/eqschemes.ml b/tactics/eqschemes.ml index 27d086095..f86c22bcf 100644 --- a/tactics/eqschemes.ml +++ b/tactics/eqschemes.ml @@ -563,7 +563,7 @@ let fix_r2l_forward_rew_scheme c = (Reductionops.whd_beta Evd.empty (applist (c, extended_rel_list 3 indargs @ [mkRel 1;mkRel 3;mkRel 2])))))) - | _ -> anomaly "Ill-formed non-dependent left-to-right rewriting scheme" + | _ -> anomaly (Pp.str "Ill-formed non-dependent left-to-right rewriting scheme") (**********************************************************************) (* Build the right-to-left rewriting lemma for conclusion associated *) -- cgit v1.2.3