From 928e1c69588a2057c8d30a2bb4c3fe140cfe025f Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 7 Jan 2009 20:48:01 +0000
Subject: Uniformisation of some error messages + added test on setoid rewrite.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11765 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 library/lib.ml                   |  4 ++--
 test-suite/success/setoid_test.v | 14 ++++++++++++++
 2 files changed, 16 insertions(+), 2 deletions(-)

diff --git a/library/lib.ml b/library/lib.ml
index 7135a93cc0..dfe00fae51 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -575,11 +575,11 @@ let close_section id =
       | oname,OpenedSection (_,fs) -> 
 	  let id' = basename (fst oname) in 
 	    if id <> id' then 
-	      errorlabstrm "close_section" (str "last opened section is " ++ pr_id id');
+	      errorlabstrm "close_section" (str "Last opened section is " ++ pr_id id' ++ str ".");
 	    (oname,fs)
       | _ -> assert false 
     with Not_found ->
-      error "no opened section"
+      error "No opened section."
   in
   let (secdecls,secopening,before) = split_lib oname in
   lib_stk := before;
diff --git a/test-suite/success/setoid_test.v b/test-suite/success/setoid_test.v
index f49f58e5a3..be5999df58 100644
--- a/test-suite/success/setoid_test.v
+++ b/test-suite/success/setoid_test.v
@@ -116,3 +116,17 @@ Add Morphism (@f A) : f_morph.
 Proof.
 unfold rel, f. trivial.
 Qed.
+
+(* Submitted by Nicolas Tabareau *)
+(* Needs unification.ml to support environments with de Bruijn *)
+
+Goal forall
+  (f : Prop -> Prop)
+  (Q : (nat -> Prop) -> Prop)
+  (H : forall (h : nat -> Prop), Q (fun x : nat => f (h x)) <-> True)
+  (h:nat -> Prop), 
+  Q (fun x : nat => f (Q (fun b : nat => f (h x)))) <-> True.
+intros f0 Q H.
+setoid_rewrite H.
+tauto.
+Qed.
-- 
cgit v1.2.3