diff options
| author | Matthieu Sozeau | 2015-02-15 18:13:04 +0100 |
|---|---|---|
| committer | Matthieu Sozeau | 2015-02-15 18:13:04 +0100 |
| commit | aed3c876d422f4dcc0296fd4949148c697f37b1d (patch) | |
| tree | d8b75101db72241201250429b6bb1f0cb8fb15b0 | |
| parent | dbb6de3b51dad3c055cb7638fbd6a29df9a6a22d (diff) | |
Fix test-suite file. Check that definitions do work when sharing is
disabled in the kernel.
| -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 9e12b990b7..049589325e 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)$. + |