From aed3c876d422f4dcc0296fd4949148c697f37b1d Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Sun, 15 Feb 2015 18:13:04 +0100
Subject: Fix test-suite file. Check that definitions do work when sharing is
 disabled in the kernel.

---
 test-suite/bugs/closed/3309.v | 9 +++++++--
 1 file 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)$.
+
-- 
cgit v1.2.3