diff options
| author | msozeau | 2009-06-28 21:31:02 +0000 |
|---|---|---|
| committer | msozeau | 2009-06-28 21:31:02 +0000 |
| commit | 03ad47cbbf7b2456c937ffd3ebf6e0193e3868b2 (patch) | |
| tree | aa0d446e98852be87342dacd26354f41eb467249 | |
| parent | 1616e837a886419bbb73c99fbf868c460a3ee2f8 (diff) | |
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
| -rw-r--r-- | tactics/rewrite.ml4 | 2 |
1 files changed, 1 insertions, 1 deletions
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 |