Extraction: get advantage of nicer, algebraic, module types

We use the mod_type_alg and typ_expr_alg field when they aren't
 empty.  As a consequences, many signatures are now simple
 abbreviations, or "with" constructions, leading to .mli that are
 _way_ shorter this way.  Various fixups concerning the "with
 Definition" syntax. In extract_seb_spec, we propagate both the alg
 and non-alg versions of the structure, for handlying nicely the
 "with" situation, and expanding situations not possible in ocaml.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13249 85f007b7-540e-0410-9357-904b9bb8a0f7

0 files changed, 0 insertions, 0 deletions