From 03ad47cbbf7b2456c937ffd3ebf6e0193e3868b2 Mon Sep 17 00:00:00 2001
From: msozeau
Date: Sun, 28 Jun 2009 21:31:02 +0000
Subject: Raise an error and not an anomaly if a rewrite is attempted on a
 dependent argument.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12215 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 tactics/rewrite.ml4 | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4
index d89b61c460..ed873ce76e 100644
--- a/tactics/rewrite.ml4
+++ b/tactics/rewrite.ml4
@@ -193,7 +193,7 @@ let build_signature evars env m (cstrs : 'a option list) (finalcstr : 'a Lazy.t
 	    let liftarg = mkLambda (na, ty, arg) in
 	    let arg' = mkApp (Lazy.force forall_relation, [| ty ; pred ; liftarg |]) in
 	      if obj = None then evars, mkProd(na, ty, b), arg', (ty, None) :: cstrs
-	      else raise (Invalid_argument "build_signature: no constraint can apply on a dependent argument")
+	      else error "build_signature: no constraint can apply on a dependent argument"
 	  else
 	    let (evars, b', arg, cstrs) = aux env evars (subst1 mkProp b) cstrs in
 	    let ty = Reductionops.nf_betaiota (fst evars) ty in
-- 
cgit v1.2.3