diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-10-15 15:23:47 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-10-15 15:47:39 +0200 |
| commit | d03f927e1f2d066b8fdd1e156cb98a40f8dab89d (patch) | |
| tree | 350334d43cad7bb1613f9666a715f2fe836a34d1 | |
| parent | 9097aed0e4a6af73646376ee6a24f96944a1a78e (diff) | |
Fix for bug #3618.
Fix typeclass resolution which was considering as subgoals
of a tactic application unrelated pre-existing undefined evars.
| -rw-r--r-- | tactics/class_tactics.ml | 2 | ||||
| -rw-r--r-- | test-suite/bugs/closed/3618.v (renamed from test-suite/bugs/opened/3618.v) | 13 |
2 files changed, 9 insertions, 6 deletions
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index 38f1114b5..344597fcd 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -382,7 +382,7 @@ let hints_tac hints = let sgls = evars_to_goals (fun evm ev evi -> - if Typeclasses.is_resolvable evi && + if Typeclasses.is_resolvable evi && not (Evd.is_undefined s ev) && (not info.only_classes || Typeclasses.is_class_evar evm evi) then Typeclasses.mark_unresolvable evi, true else evi, false) s' diff --git a/test-suite/bugs/opened/3618.v b/test-suite/bugs/closed/3618.v index bd24c7a7d..bbce32e9e 100644 --- a/test-suite/bugs/opened/3618.v +++ b/test-suite/bugs/closed/3618.v @@ -27,10 +27,12 @@ Fixpoint IsTrunc_internal (n : trunc_index) (A : Type) : Type := Class IsTrunc (n : trunc_index) (A : Type) : Type := Trunc_is_trunc : IsTrunc_internal n A. -Instance istrunc_paths (A : Type) n `{H : IsTrunc (trunc_S n) A} (x y : A) +Definition istrunc_paths (A : Type) n `{H : IsTrunc (trunc_S n) A} (x y : A) : IsTrunc n (x = y). Admitted. +Hint Extern 4 (IsTrunc _ (_ = _)) => eapply @istrunc_paths : typeclass_instances. + Class Funext. Instance isequiv_compose A B C f g `{IsEquiv A B f} `{IsEquiv B C g} @@ -93,8 +95,9 @@ Class inO {fs : Funext} {subU : ReflectiveSubuniverse} (T : Type) := Global Instance hprop_inO {fs : Funext} {subU : ReflectiveSubuniverse} (T : Type) : IsTrunc (trunc_S minus_two) (inO T) . Admitted. -Fail Definition equiv_O_rectnd {fs : Funext} {subU : ReflectiveSubuniverse} - (P Q : Type) {Q_inO : inO_internal Q} -: IsEquiv (fun f => compose f (O_unit P)) -:= _. +(* To avoid looping class resolution *) +Hint Mode IsEquiv - - + : typeclass_instances. +Definition equiv_O_rectnd {fs : Funext} {subU : ReflectiveSubuniverse} + (P Q : Type) {Q_inO : inO_internal Q} +: IsEquiv (fun f : O P -> P => compose f (O_unit P)) := _.
\ No newline at end of file |