From e41d7212c8c768f21a2baf61bb174a57bb7438a1 Mon Sep 17 00:00:00 2001
From: msozeau
Date: Thu, 20 Mar 2008 20:56:29 +0000
Subject: Add a flag to control rewriting under lambdas. Otherwise makes some
 rewrite calls fail because an occurence is found under a lambda that was not
 found before and there are no adequate morphism declarations to make the
 rewrite succeed nor the possibility to give occurences to rewrite (yet). Only
 setoid_rewrite will try rewriting under lambda's for now. Example problem
 found in a port of the Random library. Also improved the required_library
 error message.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10704 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 interp/coqlib.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'interp')

diff --git a/interp/coqlib.ml b/interp/coqlib.ml
index 5fe0329f6b..ca3347dbbf 100644
--- a/interp/coqlib.ml
+++ b/interp/coqlib.ml
@@ -70,7 +70,7 @@ let check_required_library d =
      (dummy_loc,make_qualid (make_dirpath (List.rev prefix)) m)
 *)
 (* or failing ...*)
-    error ("Library "^(list_last d)^" has to be required first")
+    error ("Library "^(string_of_dirpath dir)^" has to be required first")
 
 (************************************************************************)
 (* Specific Coq objects *)
-- 
cgit v1.2.3