]> matita.cs.unibo.it Git - helm.git/blob - helm/EXPORT/exportcoq/provacoqInit.v
1. PrimitiveTactics.new_metasenv_for_apply changed a little bit, moved to
[helm.git] / helm / EXPORT / exportcoq / provacoqInit.v
1 Require Export Xml.
2
3 Print XML Module Disk "examples" Datatypes.
4 Print XML Module Disk "examples" DatatypesSyntax.
5 Print XML Module Disk "examples" Logic.
6 Print XML Module Disk "examples" LogicSyntax.
7 Print XML Module Disk "examples" Specif.
8 Print XML Module Disk "examples" SpecifSyntax.
9 Print XML Module Disk "examples" Peano.
10 Print XML Module Disk "examples" Wf.
11 Print XML Module Disk "examples" Prelude.
12 Print XML Module Disk "examples" Logic_Type.
13 Print XML Module Disk "examples" Logic_TypeSyntax.