diff options
| author | Matthieu Sozeau | 2015-03-03 09:41:51 +0100 |
|---|---|---|
| committer | Matthieu Sozeau | 2015-03-03 09:41:51 +0100 |
| commit | ac62cda8a4f488b94033b108c37556877232137a (patch) | |
| tree | ea494a0816ca67c5cc00ba75712fb650ffeb380b | |
| parent | e77f178e60918f14eacd1ec0364a491d4cfd0f3f (diff) | |
Fix bug #4101, noccur_evar's expand_projection can legitimately fail
when called from w_unify, so we protect it.
| -rw-r--r-- | pretyping/evarsolve.ml | 8 | ||||
| -rw-r--r-- | test-suite/bugs/closed/4101.v | 19 |
2 files changed, 26 insertions, 1 deletions
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index 99d83a0e88..bfd19c6c7d 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -192,7 +192,13 @@ let noccur_evar env evd evk c = (match pi2 (Environ.lookup_rel i env) with | None -> () | Some b -> cache := Int.Set.add (i-k) !cache; occur_rec acc (lift i b)) - | Proj (p,c) -> occur_rec acc (Retyping.expand_projection env evd p c []) + | Proj (p,c) -> + let c = + try Retyping.expand_projection env evd p c [] + with Retyping.RetypeError _ -> + (* Can happen when called from w_unify which doesn't assign evars/metas + eagerly enough *) c + in occur_rec acc c | _ -> iter_constr_with_full_binders (fun rd (k,env) -> (succ k, push_rel rd env)) occur_rec acc c in diff --git a/test-suite/bugs/closed/4101.v b/test-suite/bugs/closed/4101.v new file mode 100644 index 0000000000..a38b050966 --- /dev/null +++ b/test-suite/bugs/closed/4101.v @@ -0,0 +1,19 @@ +(* File reduced by coq-bug-finder from original input, then from 10940 lines to 152 lines, then from 509 lines to 163 lines, then from 178 lines to 66 lines *) +(* coqc version 8.5beta1 (March 2015) compiled on Mar 2 2015 18:53:10 with OCaml 4.01.0 + coqtop version cagnode15:/afs/csail.mit.edu/u/j/jgross/coq-8.5,v8.5 (e77f178e60918f14eacd1ec0364a491d4cfd0f3f) *) + +Global Set Primitive Projections. +Set Implicit Arguments. +Record sigT {A} (P : A -> Type) := existT { projT1 : A ; projT2 : P projT1 }. +Axiom path_forall : forall {A : Type} {P : A -> Type} (f g : forall x : A, P x), + (forall x, f x = g x) -> f = g. +Lemma sigT_obj_eq +: forall (T : Type) (T0 : T -> Type) + (s s0 : forall s : sigT T0, + sigT (fun _ : T0 (projT1 s) => unit) -> + sigT (fun _ : T0 (projT1 s) => unit)), + s0 = s. +Proof. + intros. + Set Debug Tactic Unification. + apply path_forall.
\ No newline at end of file |