From dc9b65741dae1b2bf58394e26c9155dad2bf7591 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Fri, 13 Feb 2015 11:30:54 +0100 Subject: Fix test-suite file to finish --- test-suite/bugs/closed/3309.v | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) 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)$. -- cgit v1.2.3