diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2015-02-13 11:30:54 +0100 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2015-02-13 11:31:08 +0100 |
| commit | dc9b65741dae1b2bf58394e26c9155dad2bf7591 (patch) | |
| tree | a4bd3e05e91df5cf36cbaa0db80b338d351d0a51 | |
| parent | 8f73830d46d985906deadae3059db75772281516 (diff) | |
Fix test-suite file to finish
| -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)$. |