diff options
| -rw-r--r-- | test-suite/bugs/closed/3309.v | 9 |
1 files changed, 7 insertions, 2 deletions
diff --git a/test-suite/bugs/closed/3309.v b/test-suite/bugs/closed/3309.v index 9e12b990b..049589325 100644 --- a/test-suite/bugs/closed/3309.v +++ b/test-suite/bugs/closed/3309.v @@ -315,8 +315,6 @@ 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 := @@ -326,3 +324,10 @@ Definition ispartlbinopabmonoidfracrel_type : Type := Fail Timeout 1 Axiom ispartlbinopabmonoidfracrel' : $(let t:= eval unfold ispartlbinopabmonoidfracrel_type in ispartlbinopabmonoidfracrel_type in exact t)$. +Unset Kernel Term Sharing. + +Axiom ispartlbinopabmonoidfracrel : 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 + ispartlbinopabmonoidfracrel_type in exact t)$. + |