diff options
| -rw-r--r-- | test-suite/bugs/closed/3309.v | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/test-suite/bugs/closed/3309.v b/test-suite/bugs/closed/3309.v index fcebdec72..9e12b990b 100644 --- a/test-suite/bugs/closed/3309.v +++ b/test-suite/bugs/closed/3309.v @@ -315,12 +315,14 @@ Definition abmonoidfracrel ( X : abmonoid ) ( A : @submonoids X ) : hrel (@setq intros; exact (@quotrel _ _). Defined. +(* Unset Kernel Term Sharing. *) + Fail Timeout 1 Axiom ispartlbinopabmonoidfracrel : forall ( X : abmonoid ) ( A : @subabmonoids X ) { L : hrel X } ( z : abmonoidfrac X A ) , @abmonoidfracrel X A ( ( admit + z ) )admit. Definition ispartlbinopabmonoidfracrel_type : Type := forall ( X : abmonoid ) ( A : @subabmonoids X ) { L : hrel X } ( z : abmonoidfrac X A ), @abmonoidfracrel X A ( ( admit + z ) )admit. -Axiom ispartlbinopabmonoidfracrel : $(let t:= eval unfold ispartlbinopabmonoidfracrel_type in +Fail Timeout 1 Axiom ispartlbinopabmonoidfracrel' : $(let t:= eval unfold ispartlbinopabmonoidfracrel_type in ispartlbinopabmonoidfracrel_type in exact t)$. |