diff options
| author | Pierre-Marie Pédrot | 2016-02-17 18:11:02 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-02-17 18:35:27 +0100 |
| commit | 65b901534649c5f29e245a4960fa66f6e9d9c257 (patch) | |
| tree | 0acde205596fad22223998e90e6beccf433c0263 | |
| parent | f46a5686853353f8de733ae7fbd21a3a61977bc7 (diff) | |
Fix bug #4574: Anomaly: Uncaught exception Invalid_argument("splay_arity").
The setoid_rewrite tactic was not checking that the relation it was looking for
was indeed a relation, i.e. that its type was an arity.
| -rw-r--r-- | tactics/rewrite.ml | 13 | ||||
| -rw-r--r-- | test-suite/bugs/closed/4574.v | 8 |
2 files changed, 17 insertions, 4 deletions
diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml index 83742bfbdd..b04fb660d8 100644 --- a/tactics/rewrite.ml +++ b/tactics/rewrite.ml @@ -446,6 +446,8 @@ type hypinfo = { let get_symmetric_proof b = if b then PropGlobal.get_symmetric_proof else TypeGlobal.get_symmetric_proof +let error_no_relation () = error "Cannot find a relation to rewrite." + let rec decompose_app_rel env evd t = (** Head normalize for compatibility with the old meta mechanism *) let t = Reductionops.whd_betaiota evd t in @@ -461,8 +463,11 @@ let rec decompose_app_rel env evd t = | App (f, args) -> let len = Array.length args in let fargs = Array.sub args 0 (Array.length args - 2) in - mkApp (f, fargs), args.(len - 2), args.(len - 1) - | _ -> error "Cannot find a relation to rewrite." + let rel = mkApp (f, fargs) in + let ty = Retyping.get_type_of env evd rel in + let () = if not (Reduction.is_arity env ty) then error_no_relation () in + rel, args.(len - 2), args.(len - 1) + | _ -> error_no_relation () let decompose_applied_relation env sigma (c,l) = let ctype = Retyping.get_type_of env sigma c in @@ -2048,8 +2053,8 @@ let setoid_proof ty fn fallback = begin try let rel, _, _ = decompose_app_rel env sigma concl in - let evm = sigma in - let car = pi3 (List.hd (fst (Reduction.dest_prod env (Typing.unsafe_type_of env evm rel)))) in + let (sigma, t) = Typing.type_of env sigma rel in + let car = pi3 (List.hd (fst (Reduction.dest_prod env t))) in (try init_setoid () with _ -> raise Not_found); fn env sigma car rel with e -> Proofview.tclZERO e diff --git a/test-suite/bugs/closed/4574.v b/test-suite/bugs/closed/4574.v new file mode 100644 index 0000000000..39ba190369 --- /dev/null +++ b/test-suite/bugs/closed/4574.v @@ -0,0 +1,8 @@ +Require Import Setoid. + +Definition block A (a : A) := a. + +Goal forall A (a : A), block Type nat. +Proof. +Fail reflexivity. + |