From ef2c3cc02409949f19c70903a86a8181f4ed03e7 Mon Sep 17 00:00:00 2001 From: letouzey Date: Tue, 25 Oct 2011 17:27:34 +0000 Subject: First attempt at making Print Assumption compatible with opaque modules (fix #2168) We replace Global.lookup_constant by our own code that looks for a module and enters its implementation. This is still preliminary work, I would prefer to understand more completely the part about module substitutions when entering an applied functor. But this code already appears to work quite well. Anyway, since we only search for constants, we don't need to reconstitute a 100% accurate environment, as long as the same objects are in it. Note: - Digging inside module structures is slower than just using Global.lookup_constant. Hence we try to avoid it as long as we could. Only in front of axioms (or in front of constant unknown to Global) do we check whether we have an inner-module implementation for this constant. There is some memoization of the search for internal structure_body out of a module_path. - In case of inner-module axioms, we might not be able to print its type, but only its long name. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14600 85f007b7-540e-0410-9357-904b9bb8a0f7 --- library/library.mllib | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'library/library.mllib') diff --git a/library/library.mllib b/library/library.mllib index 4efb69a21..e8b5a7a4c 100644 --- a/library/library.mllib +++ b/library/library.mllib @@ -13,4 +13,4 @@ Dischargedhypsmap Goptions Decls Heads - +Assumptions \ No newline at end of file -- cgit v1.2.3