coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Fixes #7192 (Print Assumptions does not enter implementation of submodules).	Hugo Herbelin	2018-04-07
\| \| \| \| \| \|	We fix it by looking manually for the implementation at each level of nesting rather than using the signature for the n first levels and looking for the implementation only in the n+1-th level.
*	Test for bug #4269.	Pierre-Marie Pédrot	2015-09-15
\|
*	Update test-suite after 518049fe7.	Maxime Dénès	2015-09-03
\| \| \| \|	"Fetching opaque proofs" notices are not printed by default anymore.
*	Fixing output test-suite.	Pierre-Marie Pédrot	2014-07-21
\|
*	test-suite: opaque term -> opaque proof	Pierre Boutillier	2014-02-28
\|
*	Print logical name rather than path (thus allowing reproducible tests).	xclerc	2013-12-02
\|
*	Fixing some tests from the test-suite.	ppedrot	2013-09-03
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16760 85f007b7-540e-0410-9357-904b9bb8a0f7
*	First attempt at making Print Assumption compatible with opaque modules (fix ↵	letouzey	2011-10-25
	#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