diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-10-16 14:07:03 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-10-16 14:07:03 +0000 |
| commit | c8438d017307f96511e034abc9730b7f5b8e0177 (patch) | |
| tree | a5004b6cfe84e51b8a67ca6c67d44c9f7524cb11 /proofs | |
| parent | d1df4f36c4e304d6ed446d09b64d1b3bf34bac16 (diff) | |
Attempt to clarify Extract_env.extract_seb_spec
-The use of Modops.type_of_mb seems to be sometimes an overkill :
it expands the situation where mb.mod_type=SEBident...
we use a simplier my_type_of_mb instead
-No more "truetype" boolean argument to this function. Normally,
the use of my_type_of_mb should ensure that all seb we inspect
are "true" module types, see the invariant written before this
function.
-Remove the use of replicate_msid: it was commented out since
a few months, no problem appeared, and anyway the handling of
"With ..." has completely changed since Elie's work.
-And by the way, cleanup of whitespaces at the end of lines...
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11455 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'proofs')
0 files changed, 0 insertions, 0 deletions